HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Wednesday, April 13, 2011 - 6:44:14 PM
Last modification on : Wednesday, April 27, 2022 - 3:42:23 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