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 3  
Mar 5  
Mar 10  
Mar 12  
Mar 17(Spring Break) 
Mar 19(Spring Break) 
Mar 24  
Mar 26  
Mar 31  
Apr 2  
Apr 7  
Apr 9  
Apr 14  
Apr 16  
Apr 21  
Apr 23  
Apr 28  
Apr 30