Seminar and crash course on advanced type theory and formal logic (for vegetables).

- Start date: April 12, 2012.
- End date: ?

**This page is to be updated on the way.**

- Seminar meetings: every Friday at 19:30.
- Implementation meetings: from time to time.
- Place: near 147A at the main building of NRU ITMO, Kronverkskiy pr. 49, Saint Petersburg, Russia.

- Type Theory For Vegetables at Google Groups.
- @oxij (in English) and/or @neoxij (not only in English).

Implementation language: Agda [1].

Language tutorials:

- Logic-oriented introduction by Anton Setzer [@Setzer:intertheo].
- Functional-programming-oriented introduction by Ulf Norell [2].
- Videos by Daniel Peebles [3] and Conor McBride [4].
- Short and condensed introductionary talk by me at FProg meeting (in Russian) [@Malakhovski:agda-video-intro].
- There’s a list of tutorials at Agda Wiki [@agda-wiki-tutorials].

~~Striked out things~~ are topics that weren’t covered explictly. You’re expected to do them yourself.

- Type-free λ-calculus
- λ-term as a tree
- Pre-terms. Substitution lemma (stated). λ-term as a setoid ( =
_{α}) - De Bruijn representation of λ-terms
- β-reduction and
~~η-reduction~~ - Church-Rosser property (proved)
- Normal order normalization (~proved)
- Convertibility relation ( =
_{β}) - Y-combinator
- Data structures and programming in λ
- “Untyped Haskell” data and programming
~~λ interpreter in λ~~~~(μ)-recursive functions and λ~~- λ and Turing machines

- Introducing types
- Church-style
*λ*_{ → } - Some properties of
*λ*_{ → }(stated)

- Church-style
~~A bit of philosophy and suffering~~. HOWTO: Get Started with Agda (i.e. how to install and configure Agda and Emacs) | [5]- Agda
- Simple functions, datatypes and pattern matching
- Induction and termination checking
- Interactive programming with agda-mode
- Interpreter for type-free λ
- Dependent types, implicit arguments, dependent pattern matching
- Propositional equality
- Proving simple arithmetic lemmas
**Proving properties of type-free λ in Agda**

- Proof styles:
- Hilbert style
- Gentzen style
- Flat contexts

- Monomorphic systems (logic):
- Propositional logic
*λ*_{ → }**Proving properties of***λ*_{ → }in Agda- 1st order intuitionistic logic
- 1st order classical logic
- λP₁ and λP

- Monomorphic systems (semantics):
- Boolean algebras
- Heyting algebras
- Kripke models

- Monomorphic systems (arithmetic):
- Peano Arithmetic
- Heyting Arithmetic
- System T

- Polymorphic systems (logic):
- 2nd order intuitionistic logic
- 2nd order classical logic
- Hindley-Milner
- System F
- System
*F*_{ω} - Calculus of Constructions
- λ-cube

- Polymorphic systems (arithmetic):
- 2nd order PA
- 2nd order HA
- How to prove program termination in PA/HA?

- First and second order problems
- Decidability
- Type inhabitation
- Type inference:
- 1-rank type inference
- 2-rank type inference
- undecidability for 3+-rank

Universes and Pure Type Systems (PTS)

- Martin-Löf and related
- Π, Σ, W-types
- Intensional vs. extensional equality
- Observational-equality
- Homotopy type theory

- Datatypes and termination checking:
- Emulating datatypes with dependent types
- μ
- ΠΣ
- Inductive Data Types
- Type families/GADTs
- Strictly positive and Positive
- View from the left
- Levitation

- Description of real-world examples
- Agda
- CiC (Coq)

- Type Erasure and Program Extraction:
- GADTs
- Coq’s Prop/Set
- EPTS

- Languages with expected time/memory complexity:
- Linear Logic
- Log
- FP
- PSPACE

- (probably not) Other interesting stuff:
- Sequent Calculus:
- Subtyping
- Kan-exsensions for optimizations

- Church and Curry style
- Subject reduction
- Church-Rosser property
- Weak normalization
- Strong normalization
- Cut-elemination

[1] Wiki, “Agda Homepage.” [Online]. Available: http://wiki.portal.chalmers.se/agda/

[2] U. Norell, “Dependently Typed Programming in Agda.” [Online]. Available: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

[3] D. Peebles, “Introduction to Agda.” [Online]. Available: http://www.youtube.com/playlist?p=B7F836675DCE009C

[4] C. McBride, “Introduction to Dependently Typed Programming using Agda.” [Online]. Available: http://www.youtube.com/playlist?list=PL44F162A8B8CB7C87

[5] J. Malakhovski, “HOWTO: Get Started with Agda.” [Online]. Available: http://blog.oxij.org/2011/12/22/howto-get-started-with-agda/