Type Theory for Vegetables Seminar

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.

Contacts

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

Resources

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

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) | [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

Checklist

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

References