Recording and Slides

Time and Location

  • Date: Wednesday, November 29
  • Time: 11:15 AM-12:15 PM
  • Location: Luddy Hall 1104 (BLIF-1104)


The logical relations technique is widely used to prove properties of programming languages, from simple applications such as termination of the simply-typed lambda calculus, to more advanced ones such as proving noninterference for languages with information-flow security. For languages that are not strongly normalizing, one usually adapts the logical relations proof technique by using step-indexing. Doing so by hand is tedious, so Dreyer, Ahmed, and Birkedal created a temporal logic named LSLR that hides some of the work.

In this talk I give an introduction to using a step-indexed logic to define logical relations and to prove type safety of the simply-typed lambda calculus with fix (general recursion).