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

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
*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.