Типы в языках программирования, 5 курс, 2 семестр, 2016/17 — различия между версиями
Материал из SEWiki
(→Лекции) |
(→Ссылки) |
||
| Строка 27: | Строка 27: | ||
* [http://starling.rinet.ru/~goga/tapl/tapl.pdf Б. Пирс - Типы в языках программирования] | * [http://starling.rinet.ru/~goga/tapl/tapl.pdf Б. Пирс - Типы в языках программирования] | ||
* [http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism] | * [http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism] | ||
| + | * [http://oxij.org/note/BrutalDepTypes/ J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda] | ||
Версия 23:50, 21 апреля 2017
Преподаватель -- Елагин Кирилл
Лекции
Лекция 2. Простое типизированное лямбдя-исчисление
Лекция 4. АТД и рекурсивные типы
