The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.
Technical Lectures
Logical relations — Amal Ahmed
- Lecture 1 part 1 part 2 part 3
- Lecture 2 part 1 part 2 part 3
- Lecture 3 part 1 part 2 part 3
- Lecture 4 part 1 part 2 part 3
- Lecture 5 part 1 part 2 part 3
Category theory foundations — Steve Awodey
- Lecture 1 part 1 part 2 part 3
- Lecture 2 part 1 part 2 part 3
- Lecture 3 part 1 part 2 part 3
- Lecture 4 part 1 part 2 part 3
Proofs as Processes — Robert Constable
Polarization and focalization — Pierre-Louis Curien
- Notes from OPLSS 2011
- Notes from University of Bath, Feb 2012 (updated July 19, 2012)
- Strong normalisation for focalising system L
Type theory foundations — Robert Harper
Students should be familiar with
Nordstroem, Petersson, and Smith.
Programming in Martin-Loef's Type Theory.
Additionally, students might consider reading:
- Girard, Lafont and Taylor: Proofs and Types
- Harper: Practical Foundations for Programming Languages
- Pierce: Advanced Topics in Types and Programming Languages
- Normalization for Goedel's System T
- Martin-Loef: An Intuitionistic Theory of Types. In Sambin and Smith (eds), Twenty-Five Years of Constructive Type Theory, Oxford University Press
- Constable, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall.
- Lecture 1 part 1 part 2 part 3
- Lecture 2 part 1 part 2 part 3
- Lecture 3 part 1 part 2 part 3
- Lecture 4 part 1 part 2 part 3
- Lecture 5 part 1 part 2 part 3
- Lecture 6 part 1 part 2 part 3
Monads and all that — John Hughes
- Lecture 1 part 1 part 2
- Lecture 2 part 1 part 2 part 2
- Lecture 3 part 1 part 2 part 2
- Lecture 4 part 1 part 2 part 2
Compiler verification — Xavier Leroy
- Lecture 1 part 1 part 2 part 3
- Lecture 2 part 1 part 2 part 3
- Lecture 3 part 1 part 2 part 3
- Lecture 41 part 1 part 2 part 3
Language-based security — Andrew Myers
- Lecture 1 part 1 part 2 part 3
- Lecture 2 part 1 part 2 part 3
- Lecture 3 part 1 part 2
- Lecture 4 part 1 part 2 part 3
Proof theory foundations — Frank Pfenning
- Lecture 1 part 1 part 2 part 3
- Lecture 2 part 1 part 2 part 3
- Lecture 3 part 1 part 2 part 3
- Lecture 4 part 1 part 2 part 3
Software foundations in Coq — Benjamin Pierce