CIS700/009 Proof Theory for Programming Languages

TermSpring 2005
TopicProof Theory for Programming Languages
LocationLevine Hall 307
Time10:30-12:00pm, Monday and Wednesday
ProfessorsPierce, Weirich, Zdancewic
Additional resources
PrerequistesCIS500 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 Curry-Howard 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 19Algebraic semantics for classical and intuitionistic logic (2.1-2.4)Aaron
Jan 24Algebraic semantics for classical and intuitionistic logic (2.1-2.4)Aaron
Jan 26Soundness of algebraic semantics for intuitionistic logic (2.4)Aaron
Jan 31Completeness of algebraic semantics for intuitionistic logic (2.4)Aaron
Feb 2Kripke semantics for intuitionistic logic (2.5)Brian
Feb 7Completeness of Kripke semantics for intuitionistic logic (2.5)Brian
Feb 9Minimal Logic (2.6) and λ-calculus (3) Brian/Drew
Feb 14Strong normalization (4.?)Drew
Feb 16The Curry-Howard Isomorphism (4.?)Drew
Feb 21Combinators (5.?) Nate
Feb 23Combinators (5.?)Nate
Feb 28Combinators (5.?) / Type inference (6.?)Nate/Pavol
Mar 2Type inference (6.?)Pavol
Mar 7Spring Break 
Mar 9Spring Break 
Mar 14Type inference (6.?)Pavol
Mar 16YampaPaul Hudak
Mar 21Sequent Calculus (7.?) Jeff
Mar 23Sequent Calculus (7.?) Jeff
Mar 28Sequent Calculus (7.?)Jeff
Mar 30Sequent Calculus (7.?)/Classical Computation (8.?)Jeff/Dimitris
Apr 4Classical Computation (8.?)Dimitris
Apr 6Classical Computation (8.?)Dimitris
Apr 11First-order Logic (9.?)Karl
Apr 13Dependent types (10.?)Karl
Apr 18Dependent types (10.?)Karl
Apr 20Modal LogicGeoff