DagSemProc.10351.7.pdf
- Filesize: 343 kB
- 9 pages
Document
Step-Indexing: The Good, the Bad and the Ugly
Authors
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 10351
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2010-11-04
Cite AsGet BibTex
Nick Benton and Chung-Kil Hur. Step-Indexing: The Good, the Bad and the Ugly. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/DagSemProc.10351.7
https://doi.org/10.4230/DagSemProc.10351.7
Abstract
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.
Keywords
- Step-Indexing
- Logical Relations
- Low-Level Languages
- Compiler Correctness
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads