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