Teaching‎ > ‎Aarhus Mini-course‎ > ‎

Day 4

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:
  • Book: 6.1, 6.4, 6.7, 6.8, 7.1, 7.6
  • Preprint: 8.1—8.2, 8.6—8.8, 7.1
  • Ilik10: 2.2
  • Ilik09: sections 3,4
Homework: In the file Homework4.agda, there is one proof in CPS that is missing: the one for bind. Fill it in!
Č
ċ
ď
Day4-1.agda
(6k)
Danko Ilik,
Sep 20, 2012, 9:48 AM
ċ
ď
Day4-2.agda
(6k)
Danko Ilik,
Sep 20, 2012, 9:48 AM
ċ
ď
Homework4.agda
(6k)
Danko Ilik,
Sep 20, 2012, 9:48 AM
Comments