Instructor:

Steve Zdancewic
    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.

Reading and References

Grading Criteria

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

Student Presentations
3/8
Logical Step-Indexed Logical Relations
Student Presentations
3/10
No Class - Spring Break
3/15
Linear / Substructural Logics I Linear Types can Change the World!
A judgmental analysis of linear logic
Class Notes
3/17
Linear / Substructural Logics II Class Notes
3/22
Linear / Substructural Logics III Linear Logic
Class Notes
3/24
From System F to Typed Assembly Language Student Presentations
3/29
Region-Based Memory Management in Cyclone Student Presentations
3/31
Oxide: The Essence of Rust Student Presentations
4/5
RustBelt: Securing the Foundations of the Rust Programming Language Student Presentations
4/7
Rust Code Examples session_types Rust Crate
GhostCell: Separating Permissions from Data in Rust
4/12
No Class - Engagement Day
4/14
π-calculus I A Calculus of Mobile Processes, I
Class Notes
4/19
π-calculus II A theory of bisimulation for the π-calculus br> Class Notes
4/21
Session Types Caires and Pfenning 2010
Class Notes
4/26
Parallelism Par means parallel

Class Notes
4/28
Project demos / discussions Projects Due
*Prof. Zdancewic will be absent.

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.