Курс по теории типов с акцентом на практические применения: от λ-исчисления до зависимых типов, HoTT и нейро-символического AI.
λ-исчисление → STLC → System F → λω/λP → MLTT → CIC → HoTT
↓ ↓ ↓ ↓ ↓ ↓ ↓
Редукции Типы Полиморф. Завис. Coq Identity UA
α,β,η ADT ∀α.τ типы types HIT
| # | Тема | Слайды |
|---|---|---|
| 1 | Введение в λ-исчисление | |
| 2 | λ-исчисление: редукции и нормализация | |
| 3–4 | Просто типизированное λ-исчисление (STLC) | |
| 5 | ADT и алгебра типов | |
| 6 | System F (λ2) — полиморфизм второго порядка | |
| 7 | Соответствие Карри–Ховарда | |
| 8 | Субструктурные и сессионные типы | |
| 9 | λω, λP — высшие типы и зависимые типы | |
| 10 | От MLTT к Coq: CIC, Identity types | |
| 11 | Унивалентность, эквивалентности, HIT | |
| 12 | Neuro-symbolic AI & Type Theory |
| # | Тема | Формат | Ссылка |
|---|---|---|---|
| 1 | Нетипизированное λ-исчисление | LaTeX/PDF | ДЗ 1 |
| 2 | STLC, алгебра типов | LaTeX/PDF | ДЗ 2 |
| 3 | λ2, соответствие Карри–Ховарда | LaTeX/PDF | ДЗ 3 |
| 4 | Coq: базовые доказательства | Coq | ДЗ 4 |
| 5 | Coq: зависимые типы, Identity types, HoTT | Coq | ДЗ 5 |
Актуальная схема на семестр (обновлено: декабрь 2025)
- 5 домашних заданий, всего 293 балла по обязательным задачам
- Задачи со ⭐ принимаются до конца семестра
- За экзамен можно получить максимум 150 баллов
| Баллы | Оценка | % обязательных |
|---|---|---|
| 0–101 | 2 | < 35% |
| 102–189 | 3 | ≥ 35% |
| 190–262 | 4 | ≥ 65% |
| 263+ | 5 | ≥ 90% |
- Pierce — Types and Programming Languages (TAPL)
- Nederpelt, Geuvers — Type Theory and Formal Proof: An Introduction
- Barendregt — The Lambda Calculus: Its Syntax and Semantics
- Hindley, Seldin — Lambda-Calculus and Combinators: An Introduction
- Girard, Lafont, Taylor — Proofs and Types
- Sørensen, Urzyczyn — Lectures on the Curry-Howard Isomorphism
- Bertot, Castéran — Interactive Theorem Proving and Program Development (Coq'Art)
- Chlipala — Certified Programming with Dependent Types (CPDT)
- Mimram — Program = Proof
- Martin-Löf — Intuitionistic Type Theory (Bibliopolis, 1984)
- Nordström, Petersson, Smith — Programming in Martin-Löf's Type Theory
- The Agda Wiki — сайт
- HoTT Book — Homotopy Type Theory: Univalent Foundations of Mathematics — сайт
- Rijke — Introduction to Homotopy Type Theory — arXiv
- Wadler — Linear Types Can Change the World! (1990)
- Walker — Substructural Type Systems (in Advanced Topics in Types and Programming Languages)
- Bernardy et al. — Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language (POPL 2018)
- Honda — Types for Dyadic Interaction (1993)
- Vasconcelos — Fundamentals of Session Types (2012)
- Gay, Hole — Subtyping for Session Types in the Pi Calculus
- Jung et al. — RustBelt: Securing the Foundations of the Rust Programming Language (POPL 2018)
- The Rustonomicon — сайт
- Weiss et al. — Oxide: The Essence of Rust (2019)
- Trinh et al. — Solving Olympiad Geometry without Human Demonstrations (Nature, 2024)
- Yang et al. — LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (NeurIPS 2023)
- First et al. — Baldur: Whole-Proof Generation and Repair with LLMs (FSE 2023)
- Willard, Louf — Efficient Guided Generation for Large Language Models (2023) — Outlines
- Beurer-Kellner et al. — Prompting Is Programming: A Query Language for Large Language Models (PLDI 2023) — LMQL
- Lambek, Scott — Introduction to Higher Order Categorical Logic
- Awodey — Category Theory (Oxford Logic Guides)
- Crole — Categories for Types
- Oregon Programming Languages Summer School (OPLSS) — сайт
- DeepSpec Summer School — сайт
- HoTTEST Summer School — сайт — онлайн школа по HoTT
- Software Foundations (UPenn) — сайт — классика по Coq от B. Pierce
- Programming Language Foundations in Agda (PLFA) — сайт — теория типов на Agda
- Certified Programming with Dependent Types (MIT) — сайт — продвинутый курс A. Chlipala
- Introduction to Univalent Foundations (Birmingham) — сайт — HoTT на Agda, M. Escardó
- 15-814 Types and Programming Languages (CMU) — сайт — R. Harper
- 98-317 Hype for Types (CMU) — сайт — студенческий курс по теории типов
- Homotopy Type Theory (CMU) — сайт — HoTT от R. Harper
- Homotopy Type Theory (École Polytechnique) — сайт — S. Mimram
- Homotopy Type Theory (Ljubljana) — сайт — A. Bauer
- Functional Programming (Chalmers) — сайт — известный курс по Haskell и Agda
- Функциональное программирование (CSC/ВШЭ) — YouTube — другой известный курс по функциональному программированию от Д.Н. Москвина
- Semantics of Programming Languages (Cambridge) — сайт — Part II Tripos
- Introduction to HoTT (Ljubljana) — YouTube — A. Bauer
Воронов Михаил Сергеевич
michail.vms [at] gmail.com
«Типы — это исполнимые спецификации: что запрещено — не скомпилируется»