Programming Language Semantics
Course ID 15314
Description 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 focus on the most widely applicable frameworks for semantic description: denotational, operational, and axiomatic semantics. 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 imperative and functional languages, sequential and parallel, as time permits.
Key Topics
1. The denotational and operational styles of semantic description; criteria for choosing models: behavioral equivalence, compositionality, adequacy, full abstraction. A language of arithmetic expressions.
2. Sequential while-programs: direct- and continuation-style semantics. Partial and total correctness. Axiomatic semantics: Hoare logic and incorrectness logic. Declarations and scope.
3. Machine code: continuation semantics. Foundations: Scott domains, continuity and least fixed-points. A compiler for imperative programs; compiler correctness and code optimizations. Axiomatic semantics: a Hoare logic for machine code
4. Sequential pointer-programs. Abstract models of store and heap. Denotational and operational semantics. Separation logic.
5. Concurrency: shared memory models; fair execution; race conditions; safety and liveness; concurrent separation logic
6. Functional programs: types and polymorphism; call-by-value evaluation; denotational and operational semantics; progress and preservation
Learning Resources
Lecture notes and slides will be posted to canvas during the course. The following texts are suggested for optional additional reading, but they use different notation and do not cover all class material:
1. Reynolds, Theories of Programming Languages, Cambridge University Press, ISBN 0-521-59414-6.
2. Winskel, The Formal Semantics of Programming Languages: An Intro- duction, MIT Press, ISBN 0-262-23169-7.
Course Relevance
This course is designed for advanced undergraduates with interests in the mathematical and logical foundations of programming languages.
Assessment Structure
Grading is based on homeworks and a (take-home) final exam. Students are encouraged to form study groups, but each student must do homework and exams individually.
All classes will be delivered using zoom.