Decomposing Logical Relations with Forcing

Guilhem Jaber 1, 2 Nicolas Tabareau 2
2 ASCOLA - Aspect and composition languages
Inria Rennes – Bretagne Atlantique , Département informatique - EMN, LINA - Laboratoire d'Informatique de Nantes 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 metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00585717
Contributor : Guilhem Jaber <>
Submitted on : Wednesday, April 13, 2011 - 6:44:14 PM
Last modification on : Friday, June 22, 2018 - 9:28:22 AM
Long-term archiving on : Thursday, November 8, 2012 - 4:25:38 PM

File

forcing.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00585717, version 1

Citation

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

Share

Metrics

Record views

846

Files downloads

199