Lambda terms for natural deduction, sequent calculus and cut elimination

DOI10.1017/S0956796899003524MaRDI QIDQ4948037zbMATH OpenFDO

Authors Silvia Ghilezan, Henk Barendregt

Publication date 7 June 2000

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0956796899003524

zbMATH Keywords

cut eliminationnatural deduction derivationsnormal formsequent calculus derivationstype assignment systemtyped lambda termsuntyped lambda terms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05) Functional programming and lambda calculus (68N18)

Recommendations

• Linear lambda-terms and natural deduction
• scientific article; zbMATH DE number 1868900
• Lambek Calculus in Natural Deduction
• A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
• Lambda calculus and intuitionistic linear logic
• scientific article; zbMATH DE number 2024631
• Full Lambek Calculus in natural deduction
• Natural deduction and sequent calculus for intuitionistic relevant logic
• Semantics of linear/modal lambda calculus
• Typed Lambda Calculi and Applications

Cited in

(25)

• A notation for lambda terms. A generalization of environments
• Lambda terms definable as combinators
• What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
• Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment
• Proof-theoretic semantics, self-contradiction, and the format of deductive reasoning
• Classical call-by-need and duality
• A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
• Characterising Strongly Normalising Intuitionistic Sequent Terms
• Computation with classical sequents
• Completing Herbelin’s Programme
• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• Pruning simply typed  -terms
• scientific article; zbMATH DE number 871432 (Why is no real title available?)
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• Term sequent logic
• scientific article; zbMATH DE number 7089067 (Why is no real title available?)
• Controlling a population
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Refocusing Generalised Normalisation
• Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus
• Sequent calculus and equational programming
• The \(\lambda \)-calculus and the unity of structural proof theory
• Choices in representation and reduction strategies for lambda terms in intensional contexts
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage

This page was built for publication: Lambda terms for natural deduction, sequent calculus and cut elimination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4948037)