Term  Spring 2005 
Topic  Proof Theory for Programming Languages 
Location  Levine Hall 307 
Time  10:3012:00pm, Monday and Wednesday 
Professors  Pierce,
Weirich, Zdancewic 
Mailing List  CIS70000905A@lists.upenn.edu 
Texts 

Additional resources 

Prerequistes  CIS500 and CIS670 or by permission. 
Description 
Proof theory is a basic tool for research in the foundations of programming languages. We will read, together, through a selection of the basic
material in this area, concentrating on the CurryHoward Isomorphism and its ramifications. Towards the middle of the semester we will spend a couple
of weeks on basics of modal logic. The end of the semester will be devoted to exploring some of the "great works" from the programming languages
literature, with a particular eye to those with a connection to mathematical logic.
The course will be structured as a reading group with a designated "lecturer" each session; responsibility for lecturing will rotate among the
participants and grading will be based on the preparation and delivery of several lectures during the semester


Jan 19  Algebraic semantics for classical and intuitionistic logic (2.12.4)  Aaron 
Jan 24  Algebraic semantics for classical and intuitionistic logic (2.12.4)  Aaron 
Jan 26  Soundness of algebraic semantics for intuitionistic logic (2.4)  Aaron 
Jan 31  Completeness of algebraic semantics for intuitionistic logic (2.4)  Aaron 
Feb 2  Kripke semantics for intuitionistic logic (2.5)  Brian 
Feb 7  Completeness of Kripke semantics for intuitionistic logic (2.5)  Brian 
Feb 9  Minimal Logic (2.6) and λcalculus (3)  Brian/Drew 
Feb 14  Strong normalization (4.?)  Drew 
Feb 16  The CurryHoward Isomorphism (4.?)  Drew 
Feb 21  Combinators (5.?)  Nate 
Feb 23  Combinators (5.?)  Nate 
Feb 28  Combinators (5.?) / Type inference (6.?)  Nate/Pavol 
Mar 2  Type inference (6.?)  Pavol 
Mar 7  Spring Break  
Mar 9  Spring Break  
Mar 14  Type inference (6.?)  Pavol 
Mar 16  Yampa  Paul Hudak 
Mar 21  Sequent Calculus (7.?)  Jeff 
Mar 23  Sequent Calculus (7.?)  Jeff 
Mar 28  Sequent Calculus (7.?)  Jeff 
Mar 30  Sequent Calculus (7.?)/Classical Computation (8.?)  Jeff/Dimitris 
Apr 4  Classical Computation (8.?)  Dimitris 
Apr 6  Classical Computation (8.?)  Dimitris 
Apr 11  Firstorder Logic (9.?)  Karl 
Apr 13  Dependent types (10.?)  Karl 
Apr 18  Dependent types (10.?)  Karl 
Apr 20  Modal Logic  Geoff 
