Step-Indexing: The Good, the Bad and the Ugly

Modelling, Controlling and Reasoning About State

计算机科学;物理学;数学

Nick Benton ; Chung-Kil Hur

Others  :  http://drops.dagstuhl.de/opus/volltexte/2010/2808/pdf/10351.BentonNick.Paper.2808.pdf
PID  :  45062

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

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 thatstep-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.