8 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…
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…