Skip to Main content Skip to Navigation
Conference papers

MELL proof-nets in the category of graphs

Abstract : We present a formalization of proof-nets (and more generally, proofstructures) for the multiplicative-exponential fragment of linear logic, with a novel treatment of boxes: instead of integrating boxes into to the graphical structure (e.g., by adding explicit auxiliary doors, plus a mapping from boxed nodes to the main door, and ad hoc conditions on the nesting of boxes), we fix a graph morphism from the underlying graph of the proof-structure to the tree of boxes given by the nesting order. This approach allows to apply tools and notions from the theory of algebraic graph transformations, and obtain very synthetic presentations of sophisticated operations: for instance, each element of the Taylor expansion of a proof-structure is obtained by a pullback along a morphism representing a thick subtree of the tree of boxes. A treatment of cut elimination in this framework currently under development.
Document type :
Conference papers
Complete list of metadata

https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271478
Contributor : Isabelle Gouat <>
Submitted on : Friday, June 25, 2021 - 5:59:37 PM
Last modification on : Saturday, June 26, 2021 - 3:34:24 AM

File

TLLA_2021_paper_8.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License

Identifiers

  • HAL Id : lirmm-03271478, version 1

Citation

Giulio Guerrieri, Giulia Manara, Luc Pellissier, Lorenzo Tortora de Falco, Lionel Vaux Auclair. MELL proof-nets in the category of graphs. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271478⟩

Share

Metrics

Record views

85

Files downloads

20