T1: Programming with Dependent Types

Abstract

Giving more precise types to your programs means that you get more guarantees about their behaviour, but it also means that the type checker has more information about your programs and can give you more meaningful assistance during program development. In this tutorial I will give you an introduction to Agda and show how to get the system to work for you when writing dependently typed programs.

Tutorial objectives

Learn how dependent types can help you when constructing programs.

Target audience

People curious about dependent types.

Bring laptop with Agda installed (requires GHC and Emacs).

Ulf Norell

Ulf Norell has spent the last 10 years implementing the dependently typed programming language Agda at Chalmers and Gothenburg University and somehow managed to get a PhD in the process. He is currently spending half his time on Agda development at the university and the other half out in the real world doing property based testing using QuickCheck for Quviq.