Injectivity of relational semantics for (connected) MELL proof-nets via Taylor expansion

Authors :: Guerrieri, Giulio
Tortora De Falco, Lorenzo
Pellissier, Luc
Preuves, Programmes et Systèmes (PPS)
Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
Gruppo di Logica
Dipartimento di Matematica e Fisica
Università degli Studi Roma Tre-Università degli Studi Roma Tre
Laboratoire d'Informatique de Paris-Nord (LIPN)
Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)
École normale supérieure - Cachan (ENS Cachan)
Source :: 8th International Workshop on Computing with Terms and Graphs, 8th International Workshop on Computing with Terms and Graphs, Jul 2014, Vienna, Austria
Publication Year :: 2014
Publisher :: HAL CCSD, 2014.
Abstract: International audience; We show that: (1) the Taylor expansion of a cut-free MELL proof-structure R with atomic axioms is the (most informative part of the) relational semantics of R; (2) every (connected) MELL proof-net is uniquely determined by the element of order 2 of its Taylor expansion; (3) the relational semantics is injective for (connected) MELL proof-nets.

Subjects :: proof-nets
relational semantics
Taylor expansion
differential linear logic
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
denotational semantics

Language :: English
Database :: OpenAIRE
Journal :: 8th International Workshop on Computing with Terms and Graphs, 8th International Workshop on Computing with Terms and Graphs, Jul 2014, Vienna, Austria
Accession number :: edsair.dedup.wf.001..d8185929df49389e0488e6d460603b2d

Tools