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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1992
Accession Number
ADA256574

Entities

People

  • Frank Pfenning

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Algorithms
  • Calculus
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Conversion
  • Electronic Mail
  • Identities
  • Inversion
  • Judgment
  • Language
  • New York
  • Programming Languages
  • Sequences

Fields of Study

  • Mathematics

Readers

  • Computational Linguistics
  • Graph Algorithms and Convex Optimization.