Focused linear logic and the \(\lambda\)-calculus

DOI10.1016/j.entcs.2015.12.008zbMath1352.03073OpenAlexW2210298890WikidataQ113317733 ScholiaQ113317733MaRDI QIDQ5971394

Taus Brock-Nannestad, Nicolas Guenot

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

linear logiclambda calculusfocusingCurry-Howard correspondence

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)

Related Items

A Survey of the Proof-Theoretic Foundations of Logic Programming, Multi-focused cut elimination, Multi-focused proofs with different polarity assignments

Cites Work

• Linear logic
• Computational interpretations of linear logic
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Resource operators for \(\lambda\)-calculus
• On the \(\pi\)-calculus and linear logic
• Polarized proof-nets and \(\lambda \mu\)-calculus
• (Leftmost-Outermost) Beta Reduction is Invariant, Indeed
• Propositions as sessions
• The duality of computation
• Structural Focalization
• Focusing and Polarization in Intuitionistic Logic
• Focalisation and Classical Realisability
• Logic Programming with Focusing Proofs in Linear Logic
• A nonstandard standardization theorem
• Least and Greatest Fixed Points in Linear Logic
• Logical Approaches to Computational Barriers
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item