Collection of links on logical relations


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

Last updated: 2017-06-18 Sun 23:31

Emacs 25.1.1 (Org mode 9.0.5)