The \(\lambda \)-calculus and the unity of structural proof theory

DOI10.1007/S00224-009-9183-9zbMath1187.68126OpenAlexW2057240078MaRDI QIDQ733755

José Espírito Santo

Publication date: 19 October 2009

Published in: Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1822/11174

zbMATH Keywords

sequent calculusnatural deductionlambda calculusstructural proof theorytypingintuitionistic implicational logic

Mathematics Subject Classification ID

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

Related Items (3)

A resource aware semantics for a focused intuitionistic calculus ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ The polarized \(\lambda\)-calculus

Uses Software

• Pesca

Cites Work

• Combinatory logic. With two sections by William Craig.
• Permutability of proofs in intuitionistic sequent calculi
• Termination of permutative conversions in intuitionistic Gentzen calculi
• Natural deduction with general elimination rules
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Uniform proofs as a foundation for logic programming
• The duality of computation
• Structural Proof Theory as Rewriting
• Completing Herbelin’s Programme
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• A Linear Spine Calculus
• Refocusing Generalised Normalisation
• Delayed Substitutions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The \(\lambda \)-calculus and the unity of structural proof theory