by Jan Malakhovski

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

- Part 1
- First organizational meeting at April 12, 2012.
- Start date: April 13, 2012.
- End date: May 25, 2012.
- Every Friday at 19:30.

- Part 2
- Start date: September 14, 2012.
- End date: May 31, 2013.
- Every Friday at 19:30.

- Place: near 147A at the main building of NRU ITMO, Kronverkskiy pr. 49, Saint Petersburg, Russia.
- Implementation meetings: from time to time.
- Some meetings are to be substituted with Metamathematics for the more theory-minded.

- 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 [2].
- Functional-programming-oriented introduction by Ulf Norell [3].
- Videos by Daniel Peebles [4] and Conor McBride [5].
- Short and condensed introductionary talk by me at FProg meeting (in Russian) [6].
- There’s a list of tutorials at Agda Wiki [7].

~~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 ($=_\alpha$)
- De Bruijn representation of λ-terms
- β-reduction and
~~η-reduction~~ - Church-Rosser property (proved)
- Normal order normalization (~proved)
- Convertibility relation ($=_\beta$)
- Y-combinator
- Data structures and programming in λ
- “Untyped Haskell” data and programming
~~λ interpreter in λ~~~~(μ)-recursive functions and λ~~- λ and Turing machines

- Introducing types
- Church-style $\lambda_{\to}$
- Some properties of $\lambda_{\to}$ (stated)

~~A bit of philosophy and suffering~~. HOWTO: Get Started with Agda (i.e. how to install and configure Agda and Emacs) | [8]- 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
- $\lambda_{\to}$
**Proving properties of $\lambda_{\to}$ 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_{\omega}$
- 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. Agda Project Authors. Agda homepage. https://wiki.portal.chalmers.se/agda/.

2. Setzer A. Interactive theorem proving for agda users. https://web.archive.org/web/20210620074721/https://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html.

3. Norell U. Dependently typed programming in agda. 2008. https://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf.

4. Peebles D. Introduction to agda. http://www.youtube.com/playlist?p=B7F836675DCE009C.

5. McBride C. Introduction to dependently typed programming using agda. http://www.youtube.com/playlist?list=PL44F162A8B8CB7C87.

6. Malakhovski J. Введение в agda. https://www.youtube.com/watch?v=uUb-zItrYjQ.

7. Agda Project Authors. Agda: Tutorials list. 2024. https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html.

8. Malakhovski J. HOWTO: Get Started with Agda. https://blog.oxij.org/2011/12/22/howto-get-started-with-agda/.