Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types Export

@inproceedings{citeulike:5820581, abstract = {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 \&\#034;PER\&\#034; 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.}, author = {Ahmed, Amal}, booktitle = {of Lecture Notes in Computer Science}, citeulike-article-id = {5820581}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.3992}, keywords = {equivalence, logical\_relations, step\_indexed, typed}, pages = {69--83}, posted-at = {2009-09-22 14:45:42}, priority = {4}, title = {Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.3992}, volume = {3924}, year = {2006} }

TY - CONF ID - citeulike:5820581 L3 - citeulike-article-id:5820581 N2 - 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. EP - 83 TI - Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types VL - 3924 T2 - of Lecture Notes in Computer Science SP - 69 KW - equivalence KW - logical_relations KW - step_indexed KW - typed AU - Ahmed, Amal PY - 2006/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.3992 ER -