Introduction to Dependent Types and Agda

8th Summer School on Formal Techniques

  • Lecturer: Andreas Abel
  • Course: Two lectures and two tutorial sections
  • Date: 21-25 May 2018
  • Place: Menlo College, Atherton, California, USA

Abstract

Dependent types integrate programming with rich types, specifications, and verification into a single language. Dependent types allow to express arbitrary logical properties of programs, and correctness proofs can be woven into the code.

In this tutorial, I will give a brief introduction to dependent types and the dependently-typed language Agda developed at Chalmers. We will understand the theoretical concepts as we walk through some representative use cases. In the first part, we will learn how to elegantly represent binary search trees and their ordering invariant in Agda. In the second part, we will look at examples from programming language, like representation of expressions, evaluation, and equational reasoning.

The tutorial is accompanied by Agda programming and reasoning exercises.

Material

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.
  • Optionally also install the Agda standard library.

Agda tutorials

See list of tutorials on the Agda wiki, for instance:

Literature on Type Theory

This is a non-representative selection of literature, more focused on the metatheory of type theory rather than the use of type theory for verification.