Transfinite Step-Indexing: Decoupling Concrete and Logical Steps

Kasper Svendsen 1 Filip Sieczkowski 2 Lars Birkedal 3
1 CAM - University of Cambridge [UK]
2 GALLIUM - Langages de programmation, types, compilation et preuves
Inria de Paris
3 Aarhus University [Aarhus]
Abstract : Step-indexing has proven to be a powerful technique for defining logical relations for languages with advanced type systems and models of expressive program logics. In both cases, the model is stratified using natural numbers to solve a recursive equation that has no naive solutions. As a result of this stratification, current models require that each unfolding of the recursive equation – each logical step – must coincide with a concrete reduction step. This tight coupling is problematic for applications where the number of logical steps cannot be statically bounded. In this paper we demonstrate that this tight coupling between logical and concrete steps is artificial and show how to loosen it using transfinite step-indexing. We present a logical relation that supports an arbitrary but finite number of logical steps for each concrete step.
Type de document :
Communication dans un congrès
25th European Symposium on Programming Languages and Systems, Dec 2016, Eindhoven, Netherlands. 9632, pp.727 - 751, 2016, 〈10.1007/978-3-662-49498-1_28〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01408649
Contributeur : Arthur Charguéraud <>
Soumis le : mercredi 14 décembre 2016 - 11:33:42
Dernière modification le : jeudi 26 avril 2018 - 10:27:48
Document(s) archivé(s) le : mercredi 15 mars 2017 - 12:55:16

Fichier

biglater-conf (1).pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA

Citation

Kasper Svendsen, Filip Sieczkowski, Lars Birkedal. Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. 25th European Symposium on Programming Languages and Systems, Dec 2016, Eindhoven, Netherlands. 9632, pp.727 - 751, 2016, 〈10.1007/978-3-662-49498-1_28〉. 〈hal-01408649〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

113

Téléchargements de fichiers

65

Contact


archive-ouverte@inria.fr