The polarized \(\lambda\)-calculus

DOI10.1016/j.entcs.2017.04.010zbMath1394.68059OpenAlexW2646210003WikidataQ113317593 ScholiaQ113317593MaRDI QIDQ1744450

José Espírito Santo

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2017.04.010

zbMATH Keywords

focusingpolarized logicbidirectional natural deductioneta-expansiongeneral elimination rule

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

A Survey of the Proof-Theoretic Foundations of Logic Programming, A coinductive approach to proof search through typed lambda-calculi

Cites Work

• Unnamed Item
• Unnamed Item
• The \(\lambda \)-calculus and the unity of structural proof theory
• Call-by-push-value: Decomposing call-by-value and call-by-name
• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• Natural deduction with general elimination rules
• Towards a canonical classical natural deduction system
• On the unity of duality
• Structural Focalization
• Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
• Logic Programming with Focusing Proofs in Linear Logic
• Focused Natural Deduction
• Mechanizing Mathematical Reasoning