Community Profile

Здесь хорошо бы рассуждать и оставлять информацию о зависимых типах данных и смежных вопросах. Один из смежных вопросов - строгое функциональное программирование (total functional programming).

Некоторая информация для затравки:
http://lambda-the-ultimate.org - The Programming Languages Weblog, обязателен к прочтению весь (шутка).
http://e-pig.org - сайт Epigram, наиболее доступной в установке и наиболее загадочной в использовании системы программирования с зависимыми типами данных.
http://thesz.livejournal.com/670251.html?thread=4631851#t4631851 + http://thesz.livejournal.com/670954.html - про запуск Epigram под Виндовс и немного про его использование
http://lambda-the-ultimate.org/node/2003 - страничка Total Functional Programming на LtU
http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf - Generic Programming with Dependent Types, с примерами и объяснениями, 40+ страниц.
http://www.freetechbooks.com/about429.html - Programming in Martin-Lof's Type Theory: An Introduction, Nordstrom B., Smith J. M., Petersson K. Книга рассказывает про теорию типов Martin-Lof, по-моему (thesz) это одна из первых теорий зависимых типов. Судя по всему, написана аккуратно и доступно.
http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf - самая доступная статья про Observational Type System (что такое, зачем)
http://strictlypositive.org/thesis.ps.gz - диссертация Connor McBride, лежит в основе системы типов Epigram
http://www.dcs.st-and.ac.uk/~eb/writings/thesis.ps.gz - диссертация Edwin Brady о компиляции Epigram в Хаскель и устранении ненужных индексов
http://people.cs.uu.nl/andres/LambdaPi.html - Simply Easy!, реализация лямбда-исчисления с зависимыми типами путем незначительной модификации реализации simple typed lambda calculus
http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html - Simpler, Easier! Еще один вариант лямбда-исчисления с зависимыми типами. Ответ на Simply Easy! чуть выше.
http://www.dcs.st-and.ac.uk/~eb/ivor.php - библиотека на Хаскеле для встраивания в языки программирования систем зависимых типов. Использует комбинаторный подход к тактикам, основана на идеях из диссертации Connor McBride
http://www-fp.dcs.st-and.ac.uk/~eb/darcs/Ivor/ - она же, репозиторий Darcs, все самое свежее.
http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf - Type Theory and Functional Programming. Книга про зависимые типы данных, включает в себя разделы, посвященные конструктивной логике, натуральному выводу и лямбда-исчислению.
http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.HomePage - Agda2, язык программирования с зависимыми типами, имеет Emacs-режим и позволяет работать с пошаговым уточнением программы. Система типов мощнее, чем у Epigram. Вырос из системы доказательств Agda.
http://coq.inria.fr/ - The Coq proof assistant. В принципе, тоже система программирования с зависимыми типами. Умеет выдавать код на OCaml и Haskell. Классика жанра, так сказать.
http://www.cs.chalmers.se/~augustss/cayenne/index.html - Cayenne. Hotter than Haskell! Язык программирования с зависимыми типами. Это именно язык программирования. Нет ограничений на используемые в проверке типов функции. Написан на Хаскеле.
http://www.cs.chalmers.se/Cs/Research/Logic/Types/index.html - The Types Project, много всякой информации - лекции, слайды, статьи, ссылки...
http://www.cs.chalmers.se/~ulfn/ - страничка Ульфа Норелла, создателя Агды (Agda).

Желательно использование тэгов, формат произвольный. Вносите в тэги то, что вы считаете ключевой информацией. Будем разбираться с тэгами по получению представительной выборки хотя бы штук в 100 (тут выяснилось, что в ЖЖ есть ограничение на число тэгов - 1000 штук).

Members (45):

Watched by (63):