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
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.
- Introductory slides
- Lecture 1: Prelude.agda TreeSortOrd.agda
- Tutorial 1: Exercises1.agda
- Lecture 2: Lec2.zip
Individual files: EqualityWithK.agda EqualityWithoutK.agda HelloWorld.agda
Everything.agda IPL.agda Interpretation.agda Substitution.agda Normal.agda Library.agda Library-stdlib.agda Main.agda-lib
- Tutorial 2: Exercises2.agda
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).
- 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
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.
- Optionally also install the Agda standard library.
Agda tutorialsSee list of tutorials on the Agda wiki, for instance:
- Ulf Norell and James Chapman. Dependently Typed Programming in Agda. This is aimed at functional programmers.
- Ana Bove and Peter Dybjer. Dependent Types at Work. A gentle introduction including logic and proofs of programs.
Literature on Type TheoryThis is a non-representative selection of literature, more focused on the metatheory of type theory rather than the use of type theory for verification.
- 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, 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