Loïc Pujet

Summer school

Part 1: towards the Curry-Howard correspondence

(Rough) lecture notes:    summer_lecture1.pdf
Rules of simple type theory:    stt.pdf
Exercises for part 1:    summer_exercises1.pdf
Solutions:    summer_exercises1_solutions.pdf

Part 2: dependent type theory

Lecture notes:    summer_lecture2.pdf
Rules of dependent type theory:    dtt.pdf
Exercises for part 2:    summer_exercises2.pdf
Solutions:    summer_exercises2_solutions.pdf