# Type Theory. A Constructive Foundation for Logics and Computer Science

## Andreas Abel

• Area: LoCo
• Level: I
• Week: 1
• Time: 17:00 – 18:30
• Room: C2.01

#### 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).
• On Linux/Ubuntu: install the required packages: ``` apt-get install zlib1g-dev libncurses5-dev libicu-dev ```
• On Mac OS X you might have to install the ICU libraries for grapheme clusters via: ``` brew install icu4c brew link icu4c --force ```
• 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.