6 papers · 1 filter
Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco +1
We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of…
On the role of connectivity in Linear Logic proofs
Raffaele Di Donna, Lorenzo Tortora de Falco
We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structur…
Linear Realisability over nets: multiplicatives (long version)
Adrien Ragot, Thomas Seiller, Lorenzo Tortora de Falco
We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL*) and in the standard case…
Glueability of resource proof-structures: inverting the Taylor expansion (long version)
Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion charact…
Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications
Thomas Ehrhard, Maribel Fernández, Valeria de Paiva +1
This volume contains a selection of papers presented at Linearity/TLLA 2018: Joint Linearity and TLLA workshops (part of FLOC 2018) held on July 7-8, 2018 in Oxford. Linearity has…
Relational type-checking for MELL proof-structures. Part 1: Multiplicatives
Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco
Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered.…