Accession Number : ADA256574


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


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE


Personal Author(s) : Pfenning, Frank


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a256574.pdf


Report Date : Sep 1992


Pagination or Media Count : 48


Abstract : We give a detailed, informal proof of the Church-Rosser property for the untyped A-calculus and show its representation in LF. The proof is due to Tait and Martin-L6f 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 reductions and conversions.


Descriptors :   *PROGRAMMING LANGUAGES , *CALCULUS , *THEOREMS , CONVERSION , ABSTRACTS , SYNTAX , SEQUENCES , REDUCTION


Subject Categories : Numerical Mathematics
      Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE