Sciweavers

Share
ESOP
2006
Springer

Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types

9 years 25 days ago
Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types
We present a sound and complete proof technique, based on syntactic logical relations, for showing contextual equivalence of expressions in a -calculus with recursive types and impredicative universal and existential types. Our development builds on the step-indexed PER model of recursive types presented by Appel and McAllester. We have discovered that a direct proof of transitivity of that model does not go through, leaving the "PER" status of the model in question. We show how to extend the Appel-McAllester model to obtain a logical relation that we can prove is transitive, as well as sound and complete with respect to contextual equivalence. We then augment this model to support relational reasoning in the presence of quantified types. Step-indexed relations are indexed not just by types, but also by the number of steps available for future evaluation. This stratification is essential for handling various circularities, from recursive functions, to recursive types, to impr...
Amal J. Ahmed
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where ESOP
Authors Amal J. Ahmed
Comments (0)
books