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 27BindingNotes 3, PFPL 1-3
Jan 29  
Feb 3  
Feb 5  
Feb 10  
Feb 12  
Feb 17  
Feb 19  
Feb 24  
Feb 26  
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