- [конспект лекций] (https://github.com/shd/tt2018-conspect)
- [теоретические домашние задания] (https://github.com/shd/tt2021/blob/master/hw-theory.pdf)
- [материал для первой половины курса] Morten Heine B. Sørensen, Pawel Urzyczyn: Lections on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- Немного об истории
- Лямбда-выражения, синтаксис
- Булевские выражения, чёрчевские нумералы
- Morten Heine B. Sørensen, Pawel Urzyczyn: Lections on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- Альфа-эквивалентность, бета-редекс, бета-редукция
- Бета-редуцируемость и параллельная бета-редукция
- Теорема Чёрча-Россера
- Комбинаторы: определение и примеры (I,S,K)
- Рекурсия и Y-комбинаторы
- Ленивые вычисления, нормальный порядок редукции
- Morten Heine B. Sørensen, Pawel Urzyczyn: Lections on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- Язык просто типизированного исчисления (типы, контекст)
- Типизация по Чёрчу и по Карри.
- Правила вывода
- Теоремы о типизации редукции, Чёрча-Россера, об уникальности типизации по Чёрчу.
- Morten Heine B. Sørensen, Pawel Urzyczyn: Lections on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- Импликационный фрагмент интуиционистского исчисления высказываний
- Три задачи (проверка обитаемости, проверка типа, вывод типа)
- Morten Heine B. Sørensen, Pawel Urzyczyn: Lections on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- Задача унификации
- Вывод типа в просто типизированном лямбда-исчислении
- Исчисление предикатов второго порядка и система F, введение
- Morten Heine B. Sørensen, Pawel Urzyczyn: Lections on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- Правила для кванторов существования
- Экзистенциальные типы
- Morten Heine B. Sørensen, Pawel Urzyczyn: Lections on the Curry-Howard Isomorphism https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
- John C. Mitchell, Gordon D. Plotkin, Abstract Types Have Existential Type http://homepages.inf.ed.ac.uk/gdp/publications/Abstract_existential.pdf
- Ранг типа
- Аксиоматика
- Алгоритм W
- Расширения системы: экви- и изорекурсивные типы, тип для Y-комбинатора
- Luis Damas and Robin Milner, Principal type-schemes for functional programs POPL'82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, pp. 207–212
- Robin Milner, A theory of type polymorphism in programming (1978) // Journal of Computer and System Sciences, 1978, vol. 17, pp. 348--375 https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.5276
- Бенджамин Пирс, Типы в языках программирования. Издательство «Лямбда пресс» & «Добросвет», Москва, 2011
- Аксиоматика
- Лямбда-куб
- Зависимые типы, примеры зависимых типов в языках программирования
- Языки программирования на лямбда-кубе.
- Henk Barendregt, Introduction to generalized type systems. Journal of Functional Programming 1 (2): 125-154, April 1991
- Интуиционистские типовые системы для формализации доказательств
- Равенство, интенсиональные и экстенсиональные типовые системы
- Непрерывные функции
- Связные множества, линейная связность, пути
- Изоморфизм Карри-Ховарда-Воеводского
- Равенство в Аренд. Простейшие примеры программ на Аренд.
- Гомотопическая теория типов https://homotopytypetheory.org/book/
- Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. https://arxiv.org/abs/1611.02108
- Документация по языку Аренд https://arend-lang.github.io/documentation/
- Arend – язык с зависимыми типами, основанный на HoTT (часть 1) https://habr.com/ru/company/JetBrains-education/blog/469569/
- Магия: элиминатор для интервального типа coe
- Вспомогательные функции: transport, pmap
- Типы Empty и Not. Доказательство неравенства
- Документация по яызку Аренд, равенство и доказательства равенства https://arend-lang.github.io/documentation/tutorial/PartI/idtype https://arend-lang.github.io/documentation/tutorial/PartI/equalityex
- Неравенство: два способа определения (через экзистенциальный тип и через обобщённый алгебраический тип)
- rewrite и contradiction
- Set и Prop
- Документация по языку Аренд
- Универсумы
- Гомотопические уровни
- Фактор-множества, способы определения нетривиальных равенств
- Документация по языку Аренд
- Постановка задачи, необходимость дополнительной выразительной силы теории.
- Каков тип типа? Типовые системы U и U-.
- Парадокс Бурали-Форте
- Парадокс Бурали-Форте для парадоксальных универсумов (схема доказательства)
- Воспроизведение парадокса в системе U (схема), применение правила (\square,\triangle)
- Доказательство парадокса Хуркенса (варианта парадокса Жирара) на языке Coq https://coq.inria.fr/library/Coq.Logic.Hurkens.html
- Antonius J. S. Hurkens. A Simplification of Girard's Paradox
- Конструктивная аксиома выбора и её доказуемость.
- Сетоиды, аксиома выбора для сетоидов.
- Аксиома выбора в HoTT и Аренде (как аксиома о перестановке кванторов и пропозиционального обрезания).
- Мотивация для линейных типов: гарантия от копирования/уничтожения значений, оптимизации.
- Структурные правила (для натурального вывода) и соответствующие им комбинаторы в комбинаторном базисе BCKW.
- Линейные типы
- Реализация: уникальные типы
- Philip Wadler. A taste of linear logic
- Edsko de Vries, Rinus Plasmeijer, David M Abrahamson. Uniqueness Typing Simplified
- Общие понятия (что такое подтип, ко- и контравариантность)
- Система F<:
- Полный и ядерный вариант системы F<:
- Бенджамин Пирс, Типы в языках программирования. Издательство «Лямбда пресс» & «Добросвет». Москва, 2011
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent