Step-Indexed Biorthogonality: a Tutorial Example

Modelling, Controlling and Reasoning About State

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

Andrew Pitts

Others  :  http://drops.dagstuhl.de/opus/volltexte/2010/2806/pdf/10351.PittsAndrew.Paper.2806.pdf
PID  :  45055

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

来源: CEUR

【 摘 要 】

The purpose of this note is to illustrate the use of step-indexing [2] combined with biorthogonality [10, 9] to construct syntactical logical relations. It walks through the details of a syntactically simple, yet non-trivial example: a proof of the “CIU Theorem” for contextual equivalence in the untyped call-by-value l-calculus with recursively defined functions. I took as inspiration two works: Ahmed’s step-indexed syntactic logical relations for recursive types [1] and Benton & Hur’s work on compiler correctness that combines biorthogonality with step-indexing [4]. The logical relation constructed here will come as no surprise to those familiar with these works. However, compared with Ahmed, we do not regardbiorthogonality as “complex machinery” to be avoided—in my view it simplifies matters; and compared with Benton & Hur, I work entirely with operational semantics and with a high-level language. Both things are true of the recent work by Dreyer et al [7]; indeed I believe everything in this note can be deduced from their logical relation for call-by-value System F extended with recursive types, references and continuations. Nevertheless, it seems useful, for tutorial purposes, to extract a specific example of what the combination of step-indexing and biorthogonality can achieve, in as simple yet non-trivial a setting as possible. [First Paragraph]