Confluence for proof-nets via parallel cut elimination

DOI10.29007/VKFNMaRDI QIDQ7025173zbMATH OpenFDO

Authors Giulio Guerrieri, Giulia Manara, Lorenzo Tortora de Falco, Lionel Vaux Auclair

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/VKFN

zbMATH Keywords

confluencecut eliminationhypergraphslinear logicparallel reductionproof net

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cites work

• A category-theoretical approach to hypergraphs
• A semantic measure of the execution time in linear logic
• An abstract factorization theorem for explicit substitutions
• Combinatory logic. With two sections by William Craig.
• Computing connected proof(-structure)s from their Taylor expansion
• Directed hypergraphs and applications
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Factorization and normalization, essentially
• Glueability of resource proof-structures: inverting the Taylor expansion
• Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
• scientific article; zbMATH DE number 786499 (Why is no real title available?)
• scientific article; zbMATH DE number 1405619 (Why is no real title available?)
• scientific article; zbMATH DE number 7471682 (Why is no real title available?)
• Linear logic
• Parallel reductions in \(\lambda\)-calculus
• Polarized proof-nets and \(\lambda \mu\)-calculus
• Proof-net as graph, Taylor expansion as pullback
• Strong normalization property for second order linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The structure of multiplicatives

This page was built for publication: Confluence for proof-nets via parallel cut elimination

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