Accession Number:

ADA256574

Title:

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

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1992-09-01

Pagination or Media Count:

48.0

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.

Subject Categories:

  • Numerical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE