| Term | Spring 2005 |
| Topic | Proof Theory for Programming Languages |
| Location | Levine Hall 307 |
| Time | 10:30-12:00pm, Monday and Wednesday |
| Professors | Pierce,
Weirich, Zdancewic |
| Mailing List | CIS700-009-05A@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 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 19 | Algebraic semantics for classical and intuitionistic logic (2.1-2.4) | Aaron |
| Jan 24 | Algebraic semantics for classical and intuitionistic logic (2.1-2.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 Curry-Howard 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 | First-order Logic (9.?) | Karl |
| Apr 13 | Dependent types (10.?) | Karl |
| Apr 18 | Dependent types (10.?) | Karl |
| Apr 20 | Modal Logic | Geoff |
|
