Programming Language Semantics

Course ID 15812

Doctoral Breadth Course: Programming Languages - (*)
Classes marked with "*" (star) are appropriate for any CSD doctoral or 5th year master's student.

This lecture course introduces the foundational concepts and techniques of programming language semantics. The aim is to demonstrate the utility of a scientific approach, based on mathematics and logic, with applications to program analysis, language design, and compiler correctness. We introduce the concepts and techniques associated with the most well established and generally applicable frameworks for semantic description: the denotational, operational, and axiomatic styles of semantic description. We use semantics to analyze program behavior, guide the development of correct programs, prove correctness of a compiler, validate logics for program correctness, and derive general laws of program equivalence. We will discuss a variety of imperative and functional languages, sequential and parallel, as time permits.

Key Topics
We will cover a subset of the following topics, as time permits.
1. Introduction to semantics: denotational and operational. A language for binary arithmetic.
2. A language of while-programs: state transformations; loop invariants, partial and total correctness.
3. A machine code language: continuation semantics; compiling while-programs; a logic for machine code.
4. Pointers and mutable state: stores and heaps; safety, frame properties and separation logic.
5. Functional programs: types and polymorphism; call-by-value evaluation; progress and preservation

Along the way, we will introduce foundational concepts such as Scott domains, continuity principles, and fixed-point properties, which have traditionally formed the basis for semantic investigation and have been used widely.

Learning Resources
Lecture notes and slides will be made available on canvas.
The following text is recommended for extra background reading, but be warned that it uses different notation and does not cover the same material: John Reynolds: Theories of Programming Languages, Cambridge University Press, ISBN 0-521-59414-6.

Course Relevance
This is a star (*) course for CS graduate students. Graduate students in other departments, and advanced undergraduates, can take the course with the permission of the instructor. Undergraduates should register for 15-314.

Pre-required Knowledge
Strong math skills and ability to write logical proofs.

Assessment Structure
Grading is based on homework and a (take-home) final exam. Students are encouraged to form study groups, but each student must do homework and exams individually.