CS 740: Topics in Logic and Computation

CS 740: Topics in Logic and Computation

Course Contents:

Curry-Howard isomorphism between typed terms of formal systems representing computable functions and deductions in certain logics.

Simply typed lambda calculus, Godel's system T and Girard's system F. Strong normalization. Semantics. Expressibility of these -- how higher order functions and polymorphism add to expressibility.

Connection with provably recursive functions in systems of arithmetic. Polynomial time logic.

Books and References:

J.-Y. Girard, Y. Lafont, and P. Taylor.Proofs and Types, Cambridge University Press, 1989.

Notes on HOL by MJC Gordon, et. al.

Other relevant literature.