A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework Export

@article{citeulike:1639223, abstract = {We give a detailed, informal proof of the Church-Rosser property for the untyped -calculus and show its representation in LF. The proof is due to Tait and Martin-Lof and is based on the notion of parallel reduction. The representation employs higher-order abstract syntax and the judgments-as-types principle and takes advantage of term reconstruction as it is provided in the Elf implementation of LF. Proofs of meta-theorems are represented as higher-level judgments which relate sequences of...}, author = {Pfenning, Frank}, citeulike-article-id = {1639223}, citeulike-linkout-0 = {http://citeseer.ist.psu.edu/pfenning92proof.html}, citeulike-linkout-1 = {http://citeseer.lcs.mit.edu/pfenning92proof.html}, citeulike-linkout-2 = {http://citeseer.ifi.unizh.ch/pfenning92proof.html}, citeulike-linkout-3 = {http://citeseer.comp.nus.edu.sg/pfenning92proof.html}, journal = {Journal of Automated Reasoning}, keywords = {type-theory}, posted-at = {2007-09-09 17:09:48}, priority = {2}, title = {A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework}, url = {http://citeseer.ist.psu.edu/pfenning92proof.html}, year = {1993} }

TY - JOUR ID - citeulike:1639223 L3 - citeulike-article-id:1639223 N2 - We give a detailed, informal proof of the Church-Rosser property for the untyped -calculus and show its representation in LF. The proof is due to Tait and Martin-Lof and is based on the notion of parallel reduction. The representation employs higher-order abstract syntax and the judgments-as-types principle and takes advantage of term reconstruction as it is provided in the Elf implementation of LF. Proofs of meta-theorems are represented as higher-level judgments which relate sequences of... JF - Journal of Automated Reasoning TI - A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework KW - type-theory AU - Pfenning, Frank PY - 1993/// UR - http://citeseer.ist.psu.edu/pfenning92proof.html ER -