Aarhus University Seal / Aarhus Universitets segl

Transfinite step-indexing: Decoupling concrete and logical steps

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Kasper Svendsen, Cambridge University
  • ,
  • Filip Sieczkowski, INRIA Institut National de Rechereche en Informatique et en Automatique
  • ,
  • Lars Birkedal

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
EditorsPeter Thiemann
Number of pages25
Volume9632
PublisherSpringer VS
Publication year2016
Pages727-751
ISBN (print)9783662494974
ISBN (Electronic)978-3-662-49498-1
DOIs
Publication statusPublished - 2016
Event25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Conference

Conference25th European Symposium on Programming, ESOP 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
LandNetherlands
ByEindhoven
Periode02/04/201608/04/2016
SeriesLecture Notes in Computer Science
Volume9632
ISSN0302-9743

See relations at Aarhus University Citationformats

ID: 99447692