Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Transfinite Step-Indexing: Decoupling Concrete and Logical Steps

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Arthur Charguéraud Connect in order to contact the contributor
Submitted on : Wednesday, December 14, 2016 - 11:33:42 AM
Last modification on : Wednesday, June 8, 2022 - 12:50:03 PM
Long-term archiving on: : Wednesday, March 15, 2017 - 12:55:16 PM


biglater-conf (1).pdf
Files produced by the author(s)




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. pp.727 - 751, ⟨10.1007/978-3-662-49498-1_28⟩. ⟨hal-01408649⟩



Record views


Files downloads