Type Theory

Andreas Abel

Abstract

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.

Agda Installation

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 emacs editor (if it is not already on your system).
  • Install the GHC Haskell compiler with the cabal build system, preferably by getting the latest Haskell Platform.
  • Add $HOME/.cabal/bin to your PATH (or wherever cabal will install binaries on your system).
  • Install the latest versions of cabal-install, cpphs, alex, and happy from hackage.
    cabal update
    cabal install cabal-install
    cabal install cpphs
    cabal install alex
    cabal install happy
  • Install the latest version of Agda from hackage.
    cabal install Agda
    agda-mode setup
  • The last command adds a search path to the emacs agda2-mode.el to your .emacs file.
    Launch emacs and open a new file HelloWorld.agda.
  • 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.

Slides

Further Lecture Material

Additional References