# Type Theory for Vegetables Seminar

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

## Meetings

• 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.

## Resources

Implementation language: Agda .

Language tutorials:

• Logic-oriented introduction by Anton Setzer .
• Functional-programming-oriented introduction by Ulf Norell .
• Videos by Daniel Peebles  and Conor McBride .
• Short and condensed introductionary talk by me at FProg meeting (in Russian) .
• There’s a list of tutorials at Agda Wiki .

## Plan

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) | 
• 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
• Strictly positive and Positive
• View from the left
• Levitation
• Description of real-world examples
• Agda
• CiC (Coq)
• Type Erasure and Program Extraction:
• 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

## Checklist

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

1. Agda Project Authors. Agda homepage. http://wiki.portal.chalmers.se/agda/.

3. Norell U. Dependently typed programming in agda. 2008. http://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. http://www.youtube.com/watch?v=uUb-zItrYjQ.

7. Agda Wiki Authors. Agda tutorials list. 2015. http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials.

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