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.
Type de document :
Pré-publication, Document de travail
2011
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-00585717
Contributeur : Guilhem Jaber <>
Soumis le : mercredi 13 avril 2011 - 18:44:14
Dernière modification le : jeudi 9 février 2017 - 15:37:12
Document(s) archivé(s) le : jeudi 8 novembre 2012 - 16:25:38

Fichier

forcing.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00585717, version 1

Citation

Guilhem Jaber, Nicolas Tabareau. Decomposing Logical Relations with Forcing. 2011. 〈hal-00585717〉

Partager

Métriques

Consultations de la notice

504

Téléchargements de fichiers

167