4 papers
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…