Course Notes

• Inductive Definitions and Type Theory

• A Normalisation Proof for Gödel system T

• Some exercices on inductive definitions

• Slides for a course on inductive definitions

• Notes on typed lambda calculus (course given in Diku, 1997)

Some Exercices

• Computational content of classical logic (course given in Cambridge, 1995)