Cover Image
QR Code

A PROOF-THEORETIC TREATMENT OF λ-REDUCTION WITH CUT-ELIMINATION: λ-CALCULUS AS A LOGIC PROGRAMMING LANGUAGE.

We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic. We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform...

Full description

Published in:Journal of Symbolic Logic Vol. 76; no. 2; pp. 673 - 700
Main Author: GABBAY, MICHAEL
Format: Article
Published: Cambridge University Press Jun2011
Subjects:
Logic
Mathematics
Mathematical logic
Calculus
Mathematical analysis
Online Access:View this record in EBSCOhost