Sources on GitHub

Most course information is on Canvas.

Further course links:
Schedule on TimeEdit / Chalmers studieportal / GU ad (sv) / GU kursplan / GU course description / Course page 2025

Schedule

This schedule is preliminary!

Teachers: TC = Thierry Coquand, AA = Andreas Abel.
Room: Lecture hall MC.

Literature

Further literature and online access to books via the library can be found on Canvas.

• LN = An Introduction to Programming and Proving in Agda (draft), lecture notes
• DTW = Dependent Types at Work
• VFP = Verified Functional Programming in Agda
• TPL = Types and Programming Languages

Lectures

Lecture 1

• Introduction to formal proof
• Types in software engineering: slides
• Introduction to Agda
• Simply-typed programming in Agda

Agda code: live code start, solution, rendered

Lecture 2

• General introduction to logic and dependent types slides
• Programming and proving in Agda: Turing machines in Agda, how to formulate non termination, propositions as types slides

Agda code: bb2.agda (rendered) (Turing machines, the Busy Beaver champions, a proof that a machine never stops),
euclidean.agda (rendered) (de Bruijn’s example, the Poincaré principle),
Gentzen.agda (rendered) (natural deduction as programming),
exercises3.agda (rendered) (simple exercises on propositions as types)

Exercise 1

Getting started with Agda.
Help-session where Andreas will help you get started with Agda programming.
Before this session you need to install Agda and try to write your first Agda programs.
We’ll do some simple exercises in Agda.

Lecture 3

• Martin Löf Type Theory: principles
• Typing and equality judgements
• Formation, introduction, elimination, computation, and extensionality rules
• Positive and negative types
• Simple types: function space, cartesian product, disjoint sum, booleans and natural numbers

Slides: lecture3.pdf

Lecture 4

• Martin Löf Type Theory: dependent types
• Dependent function type
• Negative types: Π and Σ
• Positive types: ℕ
• The equality type
• Universes

2025 Lecture 3

• More on Turing machines
• Inductive predicates
• Propositional and predicate logic
• Propositions as Types, Natural Deduction in Agda

2025 Lecture 4

• Data types, induction and indexed data types
• Proof by induction on Data Types
• Indexed Data Types: typed expression
• Equality as an Indexed Data Type
• Definitional Equality versus Equality as Type (“book equality”)

Lecture 5

• Hilbert and Gentzen calculus in Agda for propositional logic with implication
• Show equivalence (deduction theorem)
• Run equivalence as proof transformation
• Untyped arithmetic expressions and operational semantics (small-step and big-step)
• Typed predicate on arithmetic expressions
• Progress and preservation theorems

Lecture 6

• General results on untyped lambda calculus:
  
• Confluence of reduction
• Equivalence from reduction
• Representation of untyped lambda calculus in Agda

Lecture 7

• Correctness of a simple compiler to stack machine with addition
• Krivine machine

Lecture 8

• Well-typed lambda-terms
• Denotational semantics for typed lambda-calculus
• Bidirectional type-checker
• Evidence-producing type-checker

Agda code (expressions in spine form, superseded by lecture 9): live code start, full, rendered

Lecture 9

Implementation of simply-typed lambda-calculus (STLC), continued.

• the parse, don’t validate principle
• bidirectional checking implemented in Agda
• with vs. case ... of \ where vs. local functions
• working with equality proofs (subst, cong)
• deciding equality
• lexer for the syntax of STLC
• grammar of STLC
• (briefly: parser monad)

Agda live code: start, finish, solution, rendered

Lecture 10

Normalization for typed lambda-calculus

• βη-equality
• weakening
• substitution
• η-long β-normal forms
• weak normalization
• reducibility

Agda live code: start, solution, rendered

Lecture 11

Possible topics:

• Confluence in Agda (Parallel substituion method)
• Machine (KAM) for classical logic (Peirce CC)

Software

We recommend Agda version 2.8.0 (recent older versions are also ok).

Installing Agda from binary

1. Download a suitable binary package from https://github.com/agda/agda/releases/tag/v2.8.0 and put it in your PATH
2. Run agda --setup

Installing Agda from source

0. Install latest Haskell (see below)
1. Install Agda from Stackage nightly: stack install --resolver=nightly Agda
2. Run agda --setup
3. Set up the Agda mode (see below)

Installing Haskell

1. Install GHCup
2. Install Stack (3.11.1) and GHC (9.12.4) from within ghcup tui
3. Ensure that the path printed by stack path --local-bin is in your system PATH

Note: if you use GHC 9.14.1 to build Agda, you need Agda 2.8.0.1 rather than 2.8.0.

Setting up the Agda mode (Emacs)

1. Compile the Emacs lisp files: agda-mode compile
2. Install the Agda mode: agda-mode setup

Setting up the Agda mode (VSCode)

Get the agda-mode extension (authored by Ting-Gian LUA).

Installing the Agda standard library

To install a library for Agda, it must be downloaded and the path to its .agda-lib file must be mentioned in the file $AGDA_APP_DIR/libraries, where $AGDA_APP_DIR is the directory printed by agda --print-agda-app-dir.
(In case this directory does not exist yet, please create it.)

For instance, to install the Agda standard library, you can follow these steps.

1. Download the version of the standard library for your Agda version according to https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary .
   For Agda 2.8.0, this is version 2.4.
   

2. Unpack the library into a directory of your choice, for instance (on Linux/MacOS):
   ~/.agda/libraries.d/standard-library

3. Recommended: in this directory rename agda-stdlib-2.4 to v2.4 (or similar).
   

4. Add the following line to your ~/.agda/libraries file (create it if it does not exist):

   ~/.agda/libraries.d/standard-library/v2.4/standard-library.agda-lib

   In this you need to expand ~ manually to your home folder.

On Windows, the libraries file might reside in another directory than ~/.agda.
Check the output of agda --print-agda-app-dir.