5 citations · 6 across the 8 of their papers we have counts for
9 papers
An explicit shuffle construction of the homotopy span model of differential linear logic
Paul-André Melliès, Federico Olimpieri, Lionel Vaux Auclair
We give a direct and explicit construction of the homotopy span model of linear logic originally formulated by Melliès using abstract homotopy theory in the Quillen category Cat of…
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…
The algebraic -calculus is a conservative extension of the ordinary -calculus
Axel Kerinec, Lionel Vaux Auclair
The algebraic -calculus is an extension of the ordinary -calculus with linear combinations of terms. We establish that two ordinary -terms are equivalent in the algebraic…
Extensional Taylor Expansion
Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair
We introduce a calculus of extensional resource terms. These are resource terms à la Ehrhard-Regnier, but in infinitely eta-long form. The calculus still retains a finite syntax an…
How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)
Rémy Cerda, Lionel Vaux Auclair
Twenty years after its introduction by Ehrhard and Regnier, differentiation in -calculus and in linear logic is now a celebrated tool. In particular, it allows to establish a Ta…
Strategies as Resource Terms, and their Categorical Semantics
Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair
As shown by Tsukada and Ong, simply-typed, normal and eta-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. The original pro…
Finitary Simulation of Infinitary -Reduction via Taylor Expansion, and Applications
Rémy Cerda, Lionel Vaux Auclair
Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of -terms has been broadly used as a tool to approximate the terms of several variants of the -ca…
On the Taylor expansion of -terms and the groupoid structure of their rigid approximants
Federico Olimpieri, Lionel Vaux Auclair
We show that the normal form of the Taylor expansion of a -term is isomorphic to its Böhm tree, improving Ehrhard and Regnier's original proof along three independent directions…
An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets
Jules Chouquet, Lionel Vaux Auclair
We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose a constraint on some paths, w…