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 (not covering J or K)
• Universes

Slides: lecture4.pdf

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

• Elimination rules and their motive: BoolRec, NatRec, listRec, TreeRec
• The elimination rule of the identity type (J); subst and cong as instances of it
• Pattern matching and eliminators; zero is not one
• The identity type is intensional: function extensionality is not provable
• Indexed inductive types: parameters and indices; Vec, Fin, the relation ≤, well-typed syntax
• Two derivations of the transitivity of ≤
• Hilbert calculus in Agda: derivations as an inductive family, the deduction theorem

Slides: lecture5.pdf

Agda code: Id5.agda (rendered) (the identity type: elimination rules and their motive, J, subst, cong),
deduction.agda (rendered) (indexed inductive types, derivations as an inductive family, the deduction theorem),
checksize.agda (rendered) (the size of the derivations built by the deduction theorem)

Lecture 6

• The deduction theorem, finished; derivations from no hypothesis as an inductive family
• How to show that a formula is not derivable: build a model, and prove soundness by induction on the derivation
• The truth tables: no atom is derivable. Peirce’s law is a classical tautology, so truth values cannot refute it
• A model with two stages of knowledge: forcing, and Peirce’s law is not derivable
• What a system of rules consists of: a raw syntax, the judgment forms, a finite list of rules
• The three judgments of a dependent type theory; the typing rules and the conversion rules, written out
• Why the premises are so many, and what dropping the redundant ones costs
• Type : Type, and the same rules in Agda

Slides: lecture6.pdf

Agda code: peirce.agda (rendered) (the truth tables, and forcing over two stages of knowledge: Peirce’s law is not derivable),
typetype.agda (rendered) (the rules of the slides, constructor for constructor, as an indexed inductive family),
minimalrules.agda (rendered) (the same theory with the redundant premises dropped, the translations both ways, and the presupposition, weakening and substitution lemmas; it imports selfcontained.agda (rendered)),
xirule.agda (rendered) (the ξ rule derived from β and function extensionality; this file postulates the two weakening lemmas, which are theorems in minimalrules.agda)

Lecture 7

• A very small programming language (booleans and natural numbers): its syntax and the one-step relation e => e'
• Values, and expressions which get stuck
• The typing relation e :: T; preservation, canonical forms and progress, hence type safety
• Big-step semantics e ⇓ v, and how it relates to the one-step relation
• A compiler to a stack machine, and its correctness proof: finding the statement which the induction can carry

Slides: lecture7.pdf

Agda code: arith1.agda (rendered) (the language, small-step semantics, typing, preservation and progress),
arithexp.agda (rendered) (a variant where progress is an inductive family, and a well-typed normal form is a value),
operational.agda (rendered) (big-step semantics and its soundness; it imports arith1.agda),
compiler.agda (rendered) (the stack machine, the compiler and its correctness, with named intermediate steps),
compiler2.agda (rendered) (the same proof term without the named steps),
Confluence.agda (rendered) (the Church-Rosser theorem for β-reduction, following Martin-Löf’s proof by parallel reduction as given in Appendix II of Barendregt’s thesis (1971), lemma by lemma; historically, this proof was one of Plotkin’s motivations for operational semantics. It uses the syntax of the rules of Type : Type from selfcontained.agda)

Lecture 8

• Well-typed lambda-terms
• Denotational semantics for typed lambda-calculus
• Normal forms and neutrals
• Refutation of Peirce via analysis of normal forms
• Kripke models revisited
• Soundness: evaluation into a Kripke model
• Completeness: a Kripke model based on weakening and neutrals
• Reification and reflection
• Normalization by evaluation (NbE): completeness following soundness

Slides: lecture8.pdf

Agda code:

• All in one: Lecture8.agda, rendered

• Removed Peirce and spines: Lecture8NoPeirce.agda, rendered

• Individual modules:

  • Intrinsically typed terms: Term.agda, rendered
  • Kripke models: KripkeModel.agda, rendered
  • Weakening: Weakening.agda, rendered
  • Normalization: NbE.agda, rendered

Lecture 9

Reduction: role and definition

• Decide an equational theory by reduction, orienting the equations
• β-reduction: small-step reduction for call-by-name lambda-calculus
• Why η-reduction and η-expansion are problematic
• Parallel substitution
• Substitution needs weakening when going under λ

Confluence properties

• Church-Rosser, confluence, diamond, local confluence ­ Single step β-reduction violates diamond since substitution duplicates terms
• Single step β-reduction is locally confluent

Confluence via parallel reduction (Tait and Martin-Löf, Takahashi)

• Parallel reduction: contract some visible redexes in one step
• Complete development: contract all visible redexes in one step
• Parallel reduction has the diamond property; thus, one-step reduction is confluent

Standard reduction

• Weak head reduction
• Standard reduction sequences, defined inductively
• Standardization: every reduction sequence can be transformed into a standard one

Agda code: entrypoint Lecture9.agda, rendered

Lecture 10

Normalization for typed lambda-calculus

• weak and strong normalization
• SN implies WN
• Newman’s lemma: SN plus local confluence implies confluence
• reducibility
• proof of weak normalization via reducibility

Agda code (rendered)

Lecture 11

• Krivine abstract machine for call-by-name evaluation
• Call-by-value lambda-calculus
• CEK (control-environment-continuation) for call-by-value

Agda code:

• Krivine machine (rendered)
• call-by-value (rendered)
• CEK machine (rendered)

2025 lectures

2025 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

2025 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

2025 Lecture 10

Normalization for typed lambda-calculus

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

Agda live code: start, solution, rendered

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.