Step-Indexing: The Good, the Bad and the Ugly
- Nick Benton ,
- Chung-Kil Hur
Modelling, Controlling and Reasoning About State, Proceedings of Dagstuhl Seminar 10351 |
Published by Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
An earlier version of this work was presented at the Workshop on Syntax and Semantics of Low-Level Languages (LOLA) in July 2010.
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.