Computing connected proof(-structure)s from their Taylor expansion

DOI10.4230/LIPICS.FSCD.2016.20MaRDI QIDQ5369485zbMATH OpenFDO

Authors Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

Publication date 17 October 2017

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2016.20

zbMATH Keywords

(differential) linear logicproof-netsrelational modelTaylor expansion

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• scientific article; zbMATH DE number 7003195
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• MELL in the calculus of structures
• The relational model is injective for multiplicative exponential linear logic
• Acyclicity and Coherence in Multiplicative Exponential Linear Logic

Cited in

(13)

• The bang calculus revisited
• Proof-net as graph, Taylor expansion as pullback
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• scientific article; zbMATH DE number 7471682 (Why is no real title available?)
• An application of parallel cut elimination in unit-free multiplicative linear logic to the Taylor expansion of proof nets
• Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
• Tight typings and split bounds, fully developed
• The relational model is injective for multiplicative exponential linear logic
• The bang calculus revisited
• Resource approximation for the -calculus
• A deep inference system for differential linear logic
• Confluence for proof-nets via parallel cut elimination

This page was built for publication: Computing connected proof(-structure)s from their Taylor expansion

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