- Area: LoCo
- Level: I
- Week: 1
- Time: 17:00 – 18:30
- Room: C2.01
Type Theory has been developed as a foundation of mathematics and computer science by logicians
like Alonzo Church (from 1930) and Per Martin-Löf (from 1970). Suitable as a basis for computer-assisted proof, it is receiving increasing interest from mathematicians (e.g. Fields medalist Vladimir Voevodsky), information technology (e.g. for verifying compilers and operating systems), and computational linguistics (Aarne Ranta’s Grammatical Framework). Type theory is based on the Curry-Howard Isomorphism, which describes a precise relationship between proofs of a proposition and programs of the corresponding type. In this course, we will study the basics of Type Theory, and practice programming and proving in Agda, an implementation of Martin-Löf Type Theory. We will cover first-order logic, induction, and coinduction from a practical perspective, but we will also take a look behind the veil at the metatheory of Type Theory: Computational interpretation, models of Type Theory and the meaning of judgements, consistency and decidability of type-checking.
To follow the Agda exercises, please install Agda. For some systems, Agda might be packaged for easy installation (e.g. homebrew for Mac OS). In general, an installation from source should be possible by the following steps:
- Install the
emacseditor (if it is not already on your system).
- Install the GHC Haskell compiler with the
cabalbuild system, preferably by getting the latest Haskell Platform.
$HOME/.cabal/binto your PATH (or wherever cabal will install binaries on your system).
- Install the latest versions of
cabal install cabal-install
cabal install cpphs
cabal install alex
cabal install happy
- Install the latest version of Agda from hackage.
cabal install Agda
- The last command adds a search path to the emacs
Launch emacs and open a new file
- Type in your first Agda code:
module HelloWorld where
- Check the file with Agda by pressing
C-c C-l(Control-c Control-l) or selecting “Load File” from the Agda menu.
- Lecture 1: Natural Deduction and the Curry-Howard Isomorphism
- Lecture 2: Dependent Types
- Lecture 3: Martin-Löf Type Theory
- Lecture 4: Agda (live-coding)
- Lecture 5: Coinduction (live-coding)
Further Lecture Material
- Scriptum for Natural Deduction and the Curry-Howard Isomorphism
- An LF representation of propositional logic in Agda
- Per Martin-Löf. An intuitionistic theory of types: Predicative part. In Logic Colloquium ‘73, pages 73–118. North-Holland, 1975
- Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin Löf ’s Type Theory: An Introduction. Clarendon Press, Oxford, 1990
- Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002
- Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoret. Comput. Sci. Cambridge University Press, 1989
- Andreas Abel. Normalization by Evaluation: Dependent Types and Impredicativity. Unpublished, 2013. Habilitation thesis, Faculty for Mathematics, Informatics, and Statistics (MIST), Ludwig-Maximilians-University Munich
- Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pages 3–12. IEEE Computer Soc. Press, 2007
- Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. Logical Meth. in Comput. Sci., 8(1:29):1–36, 2012. TYPES’10 special issue