Collection of links on logical relations
Papers
See the list at http://cs.ru.nl/~freek/courses/tt-2016/
Video recorded lectures
- Amal Ahmed’s 2015 OPLSS lectures is an introduction on the topic covering strong normalization of simply-typed $λ$-calculus, soudness of STLC, recursive types and step-indexing, parametricity for universal types and free theorems, and existential types. There is a set of lecture notes by Lau Skorstengaard.
- Amal Ahmed’s 2016 OPLSS lectures cover .., .., cross-language logical relations for compiler correctness and a typed closure conversion example (Lectures 3, 4).
- Amal Ahmed also covered mutable references (OPLSS 2012 lectures, lecture 4).