CIS 670 - Advanced Topics in Programming Languages
Spring 2021

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

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.