The Curry-Howard correspondence for classical logic: history, advantages, incoveniances. Gentzen's sequent calculus LK. Curien-Herbelin's LK-mu-mu-tilde and its lambda calculus. Critical pairs and non-confluence of reduction. Correspondence between classical and intuitionistic logic. Double negation translation (Kolmororov's, Glivenko's) as CPS translations of types (CBN, CBV). A case study of proof in continuations passing style that are not classical: extending NBE to sum type in Agda. Reading material corresponding to the lectures:
Homework: In the file Homework4.agda, there is one proof in CPS that is missing: the one for bind. Fill it in! |