Step-Indexed Biorthogonality: a Tutorial Example
Andrew M. Pitts · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2010
The purpose of this note is to illustrate the use of step-indexing combined with biorthogonality 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 $lambda$-calculus with recursively defined functions.