Collection of links on logical relations

See the list at http://cs.ru.nl/~freek/courses/tt-2016/

• 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).