2026-07-20T05:40:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2808 2024-03-06T11:09:26Z ddc:004 open_access

Step-Indexing: The Good, the Bad and the Ugly Benton, Nick Hur, Chung-Kil Step-Indexing Logical Relations Low-Level Languages Compiler Correctness Over the last decade, step-indices have been widely used for the construction of operationally-based logical relations in the presence of various kinds of recursion. We first give an argument that step-indices, or something like them, seem to be required for defining realizability relations between high-level source languages and low-level targets, in the case that the low-level allows egregiously intensional operations such as reflection or comparison of code pointers. We then show how, much to our annoyance, step-indices also seem to prevent us from exploiting such operations as aggressively as we would like in proving program transformations. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nick Benton and Chung-Kil Hur 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.10351.7 urn:nbn:de:0030-drops-28085 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.7 eng https://creativecommons.org/licenses/by/4.0/legalcode