Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Decomposing Logical Relations with Forcing

Guilhem Jaber 1, 2 Nicolas Tabareau 2
2 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : Logical relations have now the maturity to deal with program equivalence for realistic programming languages with features likes recursive types, higher-order references and first-class continuations. However, such advanced logical relations---which are defined with technical developments like step-indexing or heap abstractions using recursively defined worlds---can make a proof tedious. A lot of work has been done to hide step-indexing in proofs, using Gödel-Löb logic. But to date, step-indexes have still to appear explicitely in particular constructions, for instance when building recursive worlds in a stratified way. In this paper, we go one step further, proposing an extension of Abadi-Plotkin logic with forcing construction which enables to encapsulate reasoning about step-indexing or heap in different layers. Moreover, it gives a uniform and abstract management of step-indexing for recursive terms or types and for higher-order references.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Guilhem Jaber <>
Submitted on : Wednesday, April 13, 2011 - 6:44:14 PM
Last modification on : Monday, February 15, 2021 - 10:37:18 AM
Long-term archiving on: : Thursday, November 8, 2012 - 4:25:38 PM


Files produced by the author(s)


  • HAL Id : hal-00585717, version 1


Guilhem Jaber, Nicolas Tabareau. Decomposing Logical Relations with Forcing. 2011. ⟨hal-00585717⟩



Record views


Files downloads