Типы в языках программирования, 5 курс, 2 семестр, 2016/17 — различия между версиями

Материал из SEWiki
Перейти к: навигация, поиск
(Ссылки)
(Ссылки)
 
Строка 37: Строка 37:
 
* [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://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf H. Barendregt - Lambda Calculi with Types]
+
*[http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf H. P. Barendregt - Lambda Calculi with Types]
  
 
*[http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf H. Geuvers - Introduction to Type Theory]
 
*[http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf H. Geuvers - Introduction to Type Theory]

Текущая версия на 05:23, 2 июля 2017

Преподаватель -- Елагин Кирилл

Лекции

Лекция 1. Синтаксис и семантики

Лекция 2. Простое типизированное лямбдя-исчисление

Лекция 3. Нормализация

Лекция 4. АТД и рекурсивные типы

Лекция 5. System F

Лекция 6. System Fω

Лекция 7. Зависимые типы

Лекция 8. Чистые системы типов

Лекция 9. Проверка типов

Лекция 10. Катаморфизмы

Лекция 11. Подтипы

Лекция 12. Экзистенциальные типы

Лекция 13. Обзор: зипперы, типы-пересечения, субструктурные системы типов

Практика

Ссылки