Instructor:
Steve Zdancewice-mail: stevez (AT) cis.upenn.edu
office hours: Friday 4:00-5:00pm (and by appointment) gather.town Levine 511
Course information:
time: MW 1:30-3:00discussion / announcemnts: piazza
room: Zoom Link (see piazza)
Topics in PL Research: classic techniques and their modern applications
After setting the stage with a review of basic programming languages theory: simply-typed lambda calculus, polymorphic lambda calculus, operational semantics, denotational semantics, etc., this course will look at "classic" results, techniques, and papers from the programming languages literature and the use of those ideas in current research.
- (Typed) Lambda Calculus: syntax and semantics
- Polymorphic Lambda Calculus, Parametricity, and Logical Relations
- Bi-directional Type Checking
- Recursive Types
- "Fancy" Type Systems
- others TBD
Reading and References
- Lecture Notes on the Lambda Calculus
Peter Selinger, 2013 - Types, Abstraction and Parametric Polymorphism
John C. Reynolds, 1983 - Theorems for Free! Philip Wadler, 1989
- On Girard's "Candidats de Reducibilité"
Jean Gallier, 1989
Grading Criteria
- 50% Participation, including leading a discussion about about a course topic
- 50% Course projects (group projects)
Lecture Topics and Notes
Note: The following schedule is tentative!| Date | Topic | Handouts / Notes |
|---|---|---|
| 1/20 |
No Class - POPL | |
| 1/25 |
Untyped Lambda Calculus | Selinger's Notes Chapters 1,2 & 3 |
| 1/27 |
Simply Typed Lambda Calculus | Selinger's Notes Chapter 6 |
| 2/1 |
||
| 2/3 |
||
| 2/8 |
||
| 2/10 |
||
| 2/15 |
||
| 2/17 |
||
| 2/22 |
||
| 2/24 |
||
| 3/1 |
Project Proposals Due | |
| 3/3 |
||
| 3/8 |
||
| 3/10 |
No Class - Spring Break | |
| 3/15 |
||
| 3/17 |
||
| 3/22 |
||
| 3/24 |
||
| 3/29 |
||
| 3/31 |
||
| 4/5 |
||
| 4/7 |
||
| 4/12 |
No Class - Engagement Day | |
| 4/14 |
||
| 4/19 |
||
| 4/21 |
||
| 4/26 |
||
| 4/28 |
Projects Due |
Course Projects
Half of your grade in this class will be determined by a course project, which may be completed individually or in small groups. Projects that relate synergistically with other ongoing research are encouraged.
- Groups:
Teams for group projects will consist of one, two, or three students. - Timeline:
- March 1: 2-page Project proposals are due
- April 28: Final Project due
- Topic:
The only requirement is that the topic of the project be somehow related to the course material. Here are some ideas to get your creative juices flowing:- Write a survey paper or blog post for PL Club about some "fancy" type systems feature and its uses...
- Implement some part of the theory as a Coq development.
- Implement a program that has a non-trivial use of a "fancy" type system feature (e.g. Haskell, Rust, Scala, etc.)
- Try out some implementation of a research prototype found in one of the papers we read.