Course Description
Logical relations are a well-known method for proving type soundness of
languages and equivalence of program components. The proof method dates
back to 1967 but for decades it wasn't clear how to scale the technique to
features found in practical programming languages, such as recursive
types, dynamically allocated mutable memory, polymorphism, and
concurrency. This changed with the advent of step-indexed logical
relations in the early 2000s which eliminated the circularities that
complicated prior efforts at scaling the technique to such advanced
language features.
In this course, we'll start with the simplest proof using logical
relations, using them to prove type soundness of a simply typed language,
and gradually show how to scale the technique to a variety of advanced
programming-language features. Then we'll cover many exciting recent
applications of the technique, including compiler correctness, type safety
and security properties of advanced languages, sound language
interoperability, and specification of ABIs. We'll also briefly discuss
papers in the literature that make use of logical relations for verification of
concurrent code, proving soundness of the Rust MIR, soundness of program
reasoning on CHERI, and more.
The course will consist of lectures for most of the semester. There will
be a few homework assignments in the early part of the semester to give
students practice doing logical relations proofs. For the project,
students may either (1) select a small language, compiler pass, or
interoperability case study and prove a soundness, security or correctness
property using a logical relation, or (2) select a research paper to
present that makes use of logical relations.
Topics include:
- Normalization for the simply typed lambda calculus
- Type soundness of a simply typed language
- Step-indexed logical relations for type soundness for languages with
recursive types, mutable references, polymorphism
- Type soundness of a language with linear or affine types to track
resource usage
- Use of separation logics to speficy semantic models of types
- Binary logical relations for program equivalence in the presence of
the above features
- Representation independence and free theorems
- Logical relations for verifying compiler correctness
- Logical relations for sound language interoperability and
verification of FFIs
- Logical relations for specifying ABIs and showing compilers are ABI compliant
This course is intended primarily for PhD students; however, MS
students and undergraduates are encouraged to contact the instructor.
Prerequisites
CS 5400 (PPL) or CS 7400 (Intensive PPL), or permission from instructor.
Readings
There is no required textbook. Readings will include a few research papers
relevant to the topic being covered in lecture.
Grading
The percentages below are subject to change:
- homework assignments (lightly graded, primarily for practice with logical
relations proofs) (30%)
- project and in-class presentation (50%)
- participation in class discussion (20%)
To pick up the background material required for this course you
may want to read one of the following: