9 Search Results for "Vaux, Lionel"

Document
DOI: 10.4230/LIPIcs.FSCD.2025.12
Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Authors: Rémy Cerda, Giulio Manzonetto, and Alexis Saurin

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.
Cite as

Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.FSCD.2025.12,
  author =	{Cerda, R\'{e}my and Manzonetto, Giulio and Saurin, Alexis},
  title =	{{Ohana Trees and Taylor Expansion for the \lambdaI-Calculus: No variable gets left behind or forgotten!}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.12},
  URN =		{urn:nbn:de:0030-drops-236277},
  doi =		{10.4230/LIPIcs.FSCD.2025.12},
  annote =	{Keywords: \lambda-calculus, program approximation, Taylor expansion, \lambdaI-calculus, persistent free variables, B\"{o}hm trees, Ohana trees}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.16
Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic

Authors: Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, and Lionel Vaux Auclair

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
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 Yeo’s theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting ⅋-vertex, on a splitting ⊗-vertex, on a splitting terminal vertex, etc. The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo’s theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings.
Cite as

Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, and Lionel Vaux Auclair. Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{diguardia_et_al:LIPIcs.FSCD.2025.16,
  author =	{Di Guardia, R\'{e}mi and Laurent, Olivier and Tortora de Falco, Lorenzo and Vaux Auclair, Lionel},
  title =	{{Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.16},
  URN =		{urn:nbn:de:0030-drops-236317},
  doi =		{10.4230/LIPIcs.FSCD.2025.16},
  annote =	{Keywords: Linear Logic, Proof Net, Sequentialization, Graph Theory, Yeo’s Theorem}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.23
How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus

Authors: Rémy Cerda and Lionel Vaux Auclair

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
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 write the Taylor formula in various λ-calculi, hence providing a theory of linear approximations for these calculi. In the standard λ-calculus, this linear approximation is expressed by results stating that the (possibly) infinitary β-reduction of λ-terms is simulated by the reduction of their Taylor expansion: in terms of rewriting systems, the resource reduction (operating on Taylor approximants) is an extension of the β-reduction. In this paper, we address the converse property, conservativity: are there reductions of the Taylor approximants that do not arise from an actual β-reduction of the approximated term? We show that if we restrict the setting to finite terms and β-reduction sequences, then the linear approximation is conservative. However, as soon as one allows infinitary reduction sequences this property is broken. We design a counter-example, the Accordion. Then we show how restricting the reduction of the Taylor approximants allows to build a conservative extension of the β-reduction preserving good simulation properties. This restriction relies on uniformity, a property that was already at the core of Ehrhard and Regnier’s pioneering work.
Cite as

Rémy Cerda and Lionel Vaux Auclair. How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.STACS.2025.23,
  author =	{Cerda, R\'{e}my and Vaux Auclair, Lionel},
  title =	{{How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the \lambda-Calculus}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.23},
  URN =		{urn:nbn:de:0030-drops-228480},
  doi =		{10.4230/LIPIcs.STACS.2025.23},
  annote =	{Keywords: program approximation, quantitative semantics, lambda-calculus, linear approximation, Taylor expansion, conservativity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.13
Strategies as Resource Terms, and Their Categorical Semantics

Authors: Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
As shown by Tsukada and Ong, simply-typed, normal and η-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. Though inspiring, their proof is indirect, relying on the injectivity of the relational model {w.r.t.} both sides of the correspondence - in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization. In the present paper, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step - and our third contribution - is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential λ-calculus.
Cite as

Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Strategies as Resource Terms, and Their Categorical Semantics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{blondeaupatissier_et_al:LIPIcs.FSCD.2023.13,
  author =	{Blondeau-Patissier, Lison and Clairambault, Pierre and Vaux Auclair, Lionel},
  title =	{{Strategies as Resource Terms, and Their Categorical Semantics}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.13},
  URN =		{urn:nbn:de:0030-drops-179976},
  doi =		{10.4230/LIPIcs.FSCD.2023.13},
  annote =	{Keywords: Resource calculus, Game semantics, Categorical semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.21
Linear Lambda-Calculus is Linear

Authors: Alejandro Díaz-Caro and Gilles Dowek

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.
Cite as

Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2022.21,
  author =	{D{\'\i}az-Caro, Alejandro and Dowek, Gilles},
  title =	{{Linear Lambda-Calculus is Linear}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.21},
  URN =		{urn:nbn:de:0030-drops-163024},
  doi =		{10.4230/LIPIcs.FSCD.2022.21},
  annote =	{Keywords: Proof theory, Lambda calculus, Linear logic, Quantum computing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.25
Categorifying Non-Idempotent Intersection Types

Authors: Giulio Guerrieri and Federico Olimpieri

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.
Cite as

Giulio Guerrieri and Federico Olimpieri. Categorifying Non-Idempotent Intersection Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.25,
  author =	{Guerrieri, Giulio and Olimpieri, Federico},
  title =	{{Categorifying Non-Idempotent Intersection Types}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{25:1--25:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.25},
  URN =		{urn:nbn:de:0030-drops-134592},
  doi =		{10.4230/LIPIcs.CSL.2021.25},
  annote =	{Keywords: Linear logic, bang calculus, non-idempotent intersection types, distributors, relational semantics, combinatorial species, symmetric sequences, bicategory, categorification}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.16
Taylor expansion for Call-By-Push-Value

Authors: Jules Chouquet and Christine Tasson

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
The connection between the Call-By-Push-Value lambda-calculus introduced by Levy and Linear Logic introduced by Girard has been widely explored through a denotational view reflecting the precise ruling of resources in this language. We take a further step in this direction and apply Taylor expansion introduced by Ehrhard and Regnier. We define a resource lambda-calculus in whose terms can be used to approximate terms of Call-By-Push-Value. We show that this approximation is coherent with reduction and with the translations of Call-By-Name and Call-By-Value strategies into Call-By-Push-Value.
Cite as

Jules Chouquet and Christine Tasson. Taylor expansion for Call-By-Push-Value. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chouquet_et_al:LIPIcs.CSL.2020.16,
  author =	{Chouquet, Jules and Tasson, Christine},
  title =	{{Taylor expansion for Call-By-Push-Value}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{16:1--16:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.16},
  URN =		{urn:nbn:de:0030-drops-116594},
  doi =		{10.4230/LIPIcs.CSL.2020.16},
  annote =	{Keywords: Call-By-Push-Value, Quantitative semantics, Taylor expansion, Linear Logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.15
An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets

Authors: Jules Chouquet and Lionel Vaux Auclair

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose some constraint on switching paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction. Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfy our constraints. In the present work, we stick to the unit-free and weakening-free fragment of linear logic, which is rich enough to showcase our techniques, while allowing for a very simple kind of constraint: a bound on the number of cuts that are crossed by any switching path.
Cite as

Jules Chouquet and Lionel Vaux Auclair. An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{chouquet_et_al:LIPIcs.CSL.2018.15,
  author =	{Chouquet, Jules and Vaux Auclair, Lionel},
  title =	{{An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.15},
  URN =		{urn:nbn:de:0030-drops-96828},
  doi =		{10.4230/LIPIcs.CSL.2018.15},
  annote =	{Keywords: linear logic, proof nets, cut elimination, differential linear logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.39
Taylor Expansion, lambda-Reduction and Normalization

Authors: Lionel Vaux

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We introduce a notion of reduction on resource vectors, i.e. infinite linear combinations of resource lambda-terms. The latter form the multilinear fragment of the differential lambda-calculus introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of lambda-terms. We show that the reduction of resource vectors contains the image, through Taylor expansion, of beta-reduction in the algebraic lambda-calculus, i.e. lambda-calculus extended with weighted sums: in particular, Taylor expansion and normalization commute. We moreover exhibit a class of algebraic lambda-terms, having a normalizable Taylor expansion, subsuming both arbitrary pure lambda-terms, and normalizable algebraic lambda-terms. For these, we prove the commutation of Taylor expansion and normalization in a more denotational sense, mimicking the Böhm tree construction.
Cite as

Lionel Vaux. Taylor Expansion, lambda-Reduction and Normalization. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 39:1-39:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{vaux:LIPIcs.CSL.2017.39,
  author =	{Vaux, Lionel},
  title =	{{Taylor Expansion, lambda-Reduction and Normalization}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{39:1--39:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.39},
  URN =		{urn:nbn:de:0030-drops-76948},
  doi =		{10.4230/LIPIcs.CSL.2017.39},
  annote =	{Keywords: lambda-calculus, non-determinism, normalization, denotational semantics}
}
  • Refine by Type
  • 9 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2023
  • 1 2022
  • 1 2021
  • 1 2020
  • Show More...

  • Refine by Author
  • 4 Vaux Auclair, Lionel
  • 2 Cerda, Rémy
  • 2 Chouquet, Jules
  • 1 Blondeau-Patissier, Lison
  • 1 Clairambault, Pierre
  • Show More...

  • Refine by Series/Journal
  • 9 LIPIcs

  • Refine by Classification
  • 5 Theory of computation → Linear logic
  • 4 Theory of computation → Lambda calculus
  • 2 Theory of computation → Categorical semantics
  • 2 Theory of computation → Denotational semantics
  • 2 Theory of computation → Proof theory
  • Show More...

  • Refine by Keyword
  • 3 Taylor expansion
  • 2 Linear Logic
  • 2 Linear logic
  • 2 lambda-calculus
  • 2 program approximation
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact