CSCI-B522: Programming Language Foundations

Spring 2025

This is a graduate course on the theoretical foundations of programming languages. We will learn fundamental techniques for formally defining programming languages and for proving properties of those languages and the programs written in them. Topics will include abstract syntax with binding, operational semantics, type safety, logical relations, and observational equivalence.

By the end of the course, students will be able to:

Meta

Location: Mondays and Wednesdays, 11:10am–12:25pm, Wylie Hall 115

Instructor: Carlo Angiuli, Luddy Hall 3008

Office hours: Tuesdays, 10:00am–12:00pm, or by appointment

Syllabus: PDF (last updated 1/15/25)

Textbook: Practical Foundations for Programming Languages (author's page; eBook)

Schedule

Date Topic Reading
Jan 13Introduction to PL theory Notes 1
Jan 15Inductive definitions Notes 2, PFPL 1-2
Jan 20(MLK Day) 
Jan 22Rule induction 
Jan 27Operational semantics Notes 3, PFPL 4-6
Jan 29Type safety 
Feb 3Type safety 
Feb 5Untyped λ-calculus Notes 4, PFPL 1-3
Feb 10α-equivalence and substitution 
Feb 12Abstract binding trees; STLC Notes 5, PFPL 8.2, 10
Feb 17Statics and dynamics of STLC 
Feb 19Type safety for STLC 
Feb 24Type safety for STLC; Sum types Notes 6, PFPL 11
Feb 26Sum types 
Mar 3Guest lecture by Sam Tobin-Hochstadt 
Mar 5Type isomorphisms; extensional equality 
Mar 10Curry–Howard correspondencePFPL 12
Mar 12Midterm 
Mar 17(Spring Break) 
Mar 19(Spring Break) 
Mar 24PCF Notes 8, PFPL 19-20
Mar 26PCF; isorecursive types 
Mar 31Termination for STLCNotes 9
Apr 2  
Apr 7  
Apr 9  
Apr 14  
Apr 16  
Apr 21  
Apr 23  
Apr 28  
Apr 30