Tutorials and advanced lectures
Short courses
Summer school in Bertinoro 2007
Summer school in Göteborg 2005:
- Lecture Notes:
volume 1,
volume 2
- Extra material collected during the school (except Connor McBride's Agda and Epigram example files):
extra volume
Introduction to Type Theory
- Peter Dybjer: Inductive definitions
(slides)
- Herman Geuvers: Lambda-calculus, type systems
(notes,
exercises,
slides 1,
slides 2,
slides 3,
slides 4)
- Alexandre Miquel: Impredicative type theory
(slides 1,
slides 2,
slides 3)
- Bengt Nordström: Types, propositions and problems
(notes,
slides)
Foundations
- Thierry Coquand: Domain theoretic proofs of normalisation
for type theory (slides)
- Gilles Dowek: Mixing deductions and computations
(notes, slides)
- Per Martin-Löf: Axiom of Choice
Introduction to Systems
Advanced Applications and Tools
- Yves Bertot: Coinduction
(notes,
slides)
- Jean-Christophe Filliatre: WHY system and Proofs about programs
(notes,
slides)
- John Harrison: Decision procedures
(slides)
- Christine Paulin: Krakatoa Tool for Java Program Verification
(slides)
- Laurent Thery: Floating-point algorithms
(slides)
Dependently Typed Programming
Formalisation of Mathematics
- Jeremy Avigad: Formalising the prime number theorem, and foundations for heuristic procedures for the real numbers
(notes,
slides)
- Herman Geuvers: Fundamental theory of algebra in Coq
(slides)
- Erik Palmgren: Bishop' set theory
(slides)
- Freek Wiedijk: Formalisation of mathematics
(notes 1,
notes 2,
slides)