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 - Linear Logic
Girard, 1987 - Linear
Types Can Change the World!
Philip Wadler, 1990 - A
judgmental analysis of linear logic
Chang, Chaudhuri, and Pfenning, 2003 -
From System F to Typed Assembly Language
Greg Morrisett, David Walker, Karl Crary, and Neal Glew, 1999 -
Region-Based Memory Management in Cyclone
Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, James Cheney, 2002 -
Oxide: The Essence of Rust
Aaron Weiss, Olek Gierczak, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed, 2020 -
RustBelt: Securing the Foundations of the Rust
Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer, 2017 - A Calculus of Mobile Processes, I
Robin Milner, Joachim Parrow, and David Walker, 1992 - A theory of bisimulation for the π-calculus
Davide Sangiorgi, 1996 -
Session Types as Intuitionistic Linear Logic Propositions
Caires and Pfenning, 2010 - Par means parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Federico Aschieri, Francesco A. Genco, 2020
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!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.