Типы в языках программирования, 5 курс, 2 семестр, 2016/17 — различия между версиями
Материал из SEWiki
(→Ссылки) |
(→Лекции) |
||
| Строка 3: | Строка 3: | ||
== Лекции == | == Лекции == | ||
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/01-syntax-and-semantics.html Лекция 1. Синтакс и семантики] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/02-stlc.html Лекция 2. Простое типизированное лямбдя-исчисление] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/03-normalization-and-pfc.html Лекция 3. Нормализация] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/04-ADTs-and-mu.html Лекция 4. АТД и рекурсивные типы] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/05-System-F.html Лекция 5. System F] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/06-System-F-omega.html Лекция 6. System Fω] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/07-dependent.html Лекция 7. Зависимые типы] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/08-PTS.html Лекция 8. Чистые системы типов] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/09-type-checking-and-co.html Лекция 9. Проверка типов] |
[https://kir.elagin.me/edu/types/10-catamorphisms.html Лекция 10. Катаморфизмы] | [https://kir.elagin.me/edu/types/10-catamorphisms.html Лекция 10. Катаморфизмы] | ||
Версия 01:07, 25 апреля 2017
Преподаватель -- Елагин Кирилл
Лекции
Лекция 2. Простое типизированное лямбдя-исчисление
Лекция 4. АТД и рекурсивные типы
Лекция 8. Чистые системы типов
Практика
Ссылки
- Б. Пирс - Типы в языках программирования
- M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism
- J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda
- E Meijer, M. Fokkinga, R. Paterson - Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
- C. McBride - The Derivative of a Regular Type is its Type of One-Hole Contexts
