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)

zbMATH Keywords

normal formcut eliminationtype assignment systemnatural deduction derivationstyped lambda termssequent calculus derivationsuntyped lambda terms

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40) 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

(23)

• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Completing Herbelin’s Programme
• Term sequent logic
• scientific article; zbMATH DE number 7089067 (Why is no real title available?)
• 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?)
• Proof-theoretic semantics, self-contradiction, and the format of deductive reasoning
• Choices in representation and reduction strategies for lambda terms in intensional contexts
• Refocusing Generalised Normalisation
• A notation for lambda terms. A generalization of environments
• The \(\lambda \)-calculus and the unity of structural proof theory
• Characterising Strongly Normalising Intuitionistic Sequent Terms
• Lambda terms definable as combinators
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• 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
• A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
• Classical call-by-need and duality
• Computation with classical sequents
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• Pruning simply typed  -terms
• Controlling a population
• Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus

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)