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 - Towards a Theory of Type Structure
John C. Reynolds 1974 - Types, Abstraction and Parametric Polymorphism
John C. Reynolds, 1983 - Theorems for Free!
Philip Wadler, 1989 - On Girard's "Candidats de Reducibilité"
Jean Gallier, 1989 - Abstract Models of Memory Management
Greg Morrisett, Matthias Felleisen, Robert Harper, 1995 - Modules, Abstraction, and Parametric Polymorphism
Karl Crary, 2017 -
Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages
Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson, 2013 - On the Semantic Expressiveness of Recursive Types
Marco Patrignani, Eric Mark Martin, Dominique Devriese, 2021 - Logical Step-Indexed Logical Relations
Derek Dreyer, Amal Ahmed, and Lars Birkedal, 2011
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 I | Selinger's Notes Chapters 1,2 |
1/27 |
Untyped Lambda Calculus II |
Selinger's Notes Chapters 3, 4.1 Class Notes untyped.ml |
2/1 |
Simply Typed Lambda Calculus |
Class Notes Selinger's Notes Chapter 6 |
2/3 |
STLC: Strong Normalization |
Class Notes |
2/8 |
System F / Polymorphic Lambda Calculus |
Selinger's Notes Chapter 8 Reynolds 1974 Class Notes |
2/10 |
System F and Parametricity |
Reynolds 1983 Theorems for Free! Class Notes |
2/15 |
Parametricity and Logical Relations II |
Reynolds 1983 Theorems for Free! Class Notes |
2/17 |
Mutable State | refs.ml Example Code |
2/22 |
Mutable State II - Types and Operational Semantics | Abstract Models of Memory Management |
2/24* |
No Class (WG2.8) | |
3/1 |
Modules, Abstraction, and Parametric Polymorphism Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages |
Student Presentations Project Proposals Due |
3/3 |
On the Semantic Expressiveness of Recursive Types Logical Step-Indexed Logical Relations |
Student Presentations |
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.