Proofs and Types
August – November 2016

Administrative Details

  • Evaluation
    • Assignments 30%, midsemester exam 30%, final exam 40%
    • Copying is fatal
  • Resources
    • Proofs and Types (Jean-Yves Girard with Paul Taylor & Yves Lafont)
    • Lectures on the Curry-Howard Isomorphism (Morten Heine Sorensen & Pawel Urzyczyn)
    • Derivation and Computation (Harold Simmons)
  • Submit all assignments on Moodle only. Further instructions will be given as part of the assignments.

Course Plan

  • Untyped lambda calculus
  • (Propositional) intuitionistic logic, normalization
  • Simply typed lambda calculus
  • Curry-Howard isomorphism
  • Classical logic and control operators
  • Sequent calculus, cut elimination
  • First order logic and arithmetic
  • System T
  • System F and second order logic
  • Dependent types

Assignments

Lectures