2010/01/01 by Nick Benton, Benton, Nick, Chung-Kil Hur +1
Computer Science · #Compiler Correctness #Logic, programming, and type systems #Logical Relations #Low-Level Languages #Parallel Computing and Optimization Techniques #Software Testing and Debugging Techniques #Step-Indexing
paper · doi:10.4230/dagsemproc.10351.7
openalex publication_date 2010/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.