Abstract
At the start of this lecture, we took up and deepened the notion of logical relations introduced in the 6th lecture, first by reformulating them in a purely operational way : instead of relying on a denotational semantics of the language, we can define everything in terms of a reduction relation between terms.
The next step is to extend logical relations to delicate features of languages like OCaml : general recursive types and references (mutable data structures) that can contain functions. In both cases, the usual definition of logical relations is no longer well founded by recurrence on types. In 2001, Appel and McAllester brilliantly circumvented this problem by using another criterion of good foundation : the number of reduction steps we give ourselves to observe the properties of the terms. This technique, known as step-indexing, was extended to binary logical relations by Ahmed in 2006.
In this presentation of logical relations, demonstrations require careful and cumbersome accounting of reduction steps. Appel et al. (2007) and Dreyer et al. (2011) develop a more elegant presentation in a modal logic with modality ▷ P (" P is true later ") and satisfying Löb's law (▷ P ⇒ P) ⇒ P. This logic is none other than the internal logic of the tree topos we obtained in the 7th lecture by intuitionistic forcing on integers.
