e-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:00
discussion / 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
Types Can Change the World!
Philip Wadler, 1990
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
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
- 50% Participation, including leading a discussion about about a course topic
- 50% Course projects (group projects)
Lecture Topics and NotesNote: The following schedule is tentative!
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.
Teams for group projects will consist of one, two, or three students.
- March 1: 2-page Project proposals are due
- April 28: Final Project due
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.