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

Research output: Contribution to journalArticlepeer-review

Abstract

We build on an existing a term-sequent logic for the lambda-calculus. We formulate a general sequent system that fully integrates alpha beta eta-reductions between untyped lambda-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 proof for lambda-terms. We suggest how this allows us to view the calculus of untyped alpha beta-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).
Original languageEnglish
Pages (from-to)673 - 699
Number of pages27
JournalJOURNAL OF SYMBOLIC LOGIC
Volume76
Issue number2
Publication statusPublished - 2011

Fingerprint

Dive into the research topics of 'A PROOF-THEORETIC TREATMENT OF lambda-REDUCTION WITH CUT-ELIMINATION: lambda-CALCULUS AS A LOGIC PROGRAMMING LANGUAGE'. Together they form a unique fingerprint.

Cite this