Типы в языках программирования, 5 курс, 2 семестр, 2016/17 — различия между версиями
Материал из SEWiki
(→Лекции) |
(→Ссылки) |
||
| Строка 40: | Строка 40: | ||
* [http://oxij.org/note/BrutalDepTypes/ J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda] | * [http://oxij.org/note/BrutalDepTypes/ J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda] | ||
| + | |||
| + | * [https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf P. Wadler - Theorems for free!] | ||
* [http://cs.swan.ac.uk/~cspt/DependentTypes.pdf F. Pottier, D. Rémy - The Essence of ML Type Inference] | * [http://cs.swan.ac.uk/~cspt/DependentTypes.pdf F. Pottier, D. Rémy - The Essence of ML Type Inference] | ||
Версия 21:42, 28 мая 2017
Преподаватель -- Елагин Кирилл
Лекции
Лекция 2. Простое типизированное лямбдя-исчисление
Лекция 4. АТД и рекурсивные типы
Лекция 8. Чистые системы типов
Лекция 12. Экзистенциальные типы
Лекция 13. Обзор: зипперы, типы-пересечения, субструктурные системы типов
