Почему мне интересные системы типов

Презентация доклада в приложении. Видеозапись вот тут: http://video.yandex.ru/users/jkff/view/4/ и ещё в приложении на всякий случай.

Ссылки по теме:

• http://lambda-the-ultimate.org - если я что забыл, то это завсегда отыскать там можно,
• http://home.pipeline.com/~hbaker1/ - Henry Baker's archive of research papers, интересное про линейную логику,
• http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html - статьи Филипа Вадлера про линейнуб логику,
• http://clean.cs.ru.nl/ - язык программирования Clean, язык с, натурально, уникальными типами данных,
• http://www.cs.chalmers.se/~augustss/cayenne/index.html - Cayenne, язык с зависимыми типами данных,
• http://wiki.portal.chalmers.se/agda/agda.php - Agda2, язык с зависимыми типами данных,
• http://www.kodu.ee/~jpoial/teadus/ - про систему типов для стековых машин; см. 00index.html на предмет того, где что находится.

Немного в стороне, но интересно:

• http://web.cecs.pdx.edu/~mpj/pubs/aug.html - система типов для разбора естественных языков (английского).