The material from the lectures can be found in these sources: - Sørensen-Urzyczyin: Lectures on the Curry-Howard Isomorphism, Elsevier, 2006 (referred to as the Book)
- Sørensen-Urzyczyin: Lectures on the Curry-Howard Isomorphism, manuscript, 1998 (referred to as the Preprint)
- Danko Ilik: Constructive proofs of completeness and delimited control, PhD thesis, 2010 (referred to as Ilik10)
- Jan M. Smith: Kripke models, notes, 1998 (referred to as Smith98)
- Danko Ilik: Continuationa passing style models complete for intuitionistic logic, 2009 (referred to as Ilik09)
- Roberto Di Cosmo and Thomas Dufour: The equational theory of (N,0,1,+,×,↑) is decidable, but not finitely axiomatisable, 2005 (referred to as DiCosmoDufour05)
- Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat: Remarks on isomorphisms in typed lambda calculi with empty and sum type, 2002 (referred to as FioreDiCosmoBalat)
On each Day's web page I will indicate which sections cover the lectures' material exactly. |
|