Tutorials and advanced lectures

Short courses

• Yves Bertot:Semantics of Programming Languages in Calculus of Constructions, June 4 - 8, Chalmers, Göteborg, Sweden.
• Tarmo Uustalo:Monads and more, lectures in Nottingham and Udine 2008

Summer school in Bertinoro 2007

• Lectures and course material

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 normalisationfor type theory(slides)
• Gilles Dowek: Mixing deductions and computations(notes,slides)
• Per Martin-Löf: Axiom of Choice

Introduction to Systems

• Yves Bertot, Jean-Christophe Filliatre:Coq (notes,exercices,slides 1,slides 2)
• Catarina Coquand:Agda(slides,list of commands,exercises)
• Tobias Nipkow:Isabelle/HOL(slides,exercises)

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

• Lennart Augustsson: Dependently type programming, some examples(slides)
• Benjamin Gregoire: Compiling dependent types (slides 1,slides 2)
• Connor McBride: Dependently typed datastructures (examples 1 agda,examples 2 agda,examples 3 epigram,Epigram)

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)