We introduce a new graphical representation for multiplicative and exponential linear logic proof-structures, based only on standard labelled oriented graphs and standard notions of graph theory. The inductive structure of boxes is handled by means of a box-tree. Our proof-structures are canonical and allows for an elegant definition of their Taylor expansion by means of pullbacks.
Guerrieri, G., Pellissier, L., Tortora de Falco, L. (2019). Proof-Net as Graph, Taylor Expansion as Pullback. In Logic, Language, Information, and Computation.
Proof-Net as Graph, Taylor Expansion as Pullback
Tortora de Falco, Lorenzo
2019-01-01
Abstract
We introduce a new graphical representation for multiplicative and exponential linear logic proof-structures, based only on standard labelled oriented graphs and standard notions of graph theory. The inductive structure of boxes is handled by means of a box-tree. Our proof-structures are canonical and allows for an elegant definition of their Taylor expansion by means of pullbacks.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
