6 Search Results for "Viso, Andrés"

Document
DOI: 10.4230/LIPIcs.CSL.2026.47
Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

Authors: Pablo Barenbaum, Delia Kesner, and Mariana Milicich

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation. In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play. In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.
Cite as

Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful Call-by-Value: A Semantic Interpretation via Quantitative Types. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 47:1-47:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2026.47,
  author =	{Barenbaum, Pablo and Kesner, Delia and Milicich, Mariana},
  title =	{{Useful Call-by-Value: A Semantic Interpretation via Quantitative Types}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{47:1--47:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.47},
  URN =		{urn:nbn:de:0030-drops-254721},
  doi =		{10.4230/LIPIcs.CSL.2026.47},
  annote =	{Keywords: Lambda calculus, Evaluation strategies, Call-by-Value, Useful Evaluation, Intersection types, Quantitative models}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.7
A Verified Cost Model for Call-By-Push-Value

Authors: Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The call-by-push-value λ-calculus allows for syntactically specifying the order of evaluation as part of the term language. Hence, it serves as a unifying language for embedding various evaluation strategies including call-by-value and call-by-name. Given the impact of call-by-push-value, it is remarkable that its adequacy as a model for computational complexity theory has not yet been studied. In this paper, we show that the call-by-push-value λ-calculus is reasonable for both time and space complexity. A reasonable cost model can encode other reasonable cost models with polynomial overhead in time and constant factor overhead in space. We achieve this by encoding call-by-push-value λ-calculus into Turing machines, following a simulation strategy by Forster et al.; for the converse direction, we prove that Levy’s encoding of the call-by-value λ-calculus has reasonable complexity bounds. The main results have been formalised in the HOL4 theorem prover.
Cite as

Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. A Verified Cost Model for Call-By-Push-Value. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2025.7,
  author =	{Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
  title =	{{A Verified Cost Model for Call-By-Push-Value}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.7},
  URN =		{urn:nbn:de:0030-drops-246067},
  doi =		{10.4230/LIPIcs.ITP.2025.7},
  annote =	{Keywords: lambda calculus, formalizations of computational models, computability theory, HOL, call-by-push-value reduction, time and space complexity, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.47
A Rewriting Theory for Quantum λ-Calculus

Authors: Claudia Faggian, Gaetan Lopez, and Benoît Valiron

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Quantum lambda calculus has been studied mainly as an idealized programming language - the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus are standardization and normalization results.
Cite as

Claudia Faggian, Gaetan Lopez, and Benoît Valiron. A Rewriting Theory for Quantum λ-Calculus. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{faggian_et_al:LIPIcs.CSL.2025.47,
  author =	{Faggian, Claudia and Lopez, Gaetan and Valiron, Beno\^{i}t},
  title =	{{A Rewriting Theory for Quantum \lambda-Calculus}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{47:1--47:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.47},
  URN =		{urn:nbn:de:0030-drops-228046},
  doi =		{10.4230/LIPIcs.CSL.2025.47},
  annote =	{Keywords: quantum lambda-calculus, probabilistic rewriting, operational semantics, asymptotic normalization, principles of quantum programming languages}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.27
Encoding Tight Typing in a Unified Framework

Authors: Delia Kesner and Andrés Viso

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, i.e. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.
Cite as

Delia Kesner and Andrés Viso. Encoding Tight Typing in a Unified Framework. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 27:1-27:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.CSL.2022.27,
  author =	{Kesner, Delia and Viso, Andr\'{e}s},
  title =	{{Encoding Tight Typing in a Unified Framework}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{27:1--27:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.27},
  URN =		{urn:nbn:de:0030-drops-157479},
  doi =		{10.4230/LIPIcs.CSL.2022.27},
  annote =	{Keywords: Call-by-Push-Value, Call-by-Name, Call-by-Value, Intersection Types}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2020.4
Strong Bisimulation for Control Operators (Invited Talk)

Authors: Delia Kesner, Eduardo Bonelli, and Andrés Viso

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

Abstract
The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM. Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.
Cite as

Delia Kesner, Eduardo Bonelli, and Andrés Viso. Strong Bisimulation for Control Operators (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.CSL.2020.4,
  author =	{Kesner, Delia and Bonelli, Eduardo and Viso, Andr\'{e}s},
  title =	{{Strong Bisimulation for Control Operators}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{4:1--4:23},
  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.4},
  URN =		{urn:nbn:de:0030-drops-116473},
  doi =		{10.4230/LIPIcs.CSL.2020.4},
  annote =	{Keywords: Lambda-mu calculus, proof-nets, strong bisimulation}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2015.6
Efficient Type Checking for Path Polymorphism

Authors: Juan Edi, Andrés Viso, and Eduardo Bonelli

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract
A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over recursively specified applicative data structures. A typical pattern such functions resort to is \dataterm{x}{y} which decomposes a compound, in other words any applicative tree structure, into its parts. We study type-checking for this type system in two stages. First we propose algorithms for checking type equivalence and subtyping based on coinductive characterizations of those relations. We then formulate a syntax-directed presentation and prove its equivalence with the original one. This yields a type-checking algorithm which unfortunately has exponential time complexity in the worst case. A second algorithm is then proposed, based on automata techniques, which yields a polynomial-time type-checking algorithm.
Cite as

Juan Edi, Andrés Viso, and Eduardo Bonelli. Efficient Type Checking for Path Polymorphism. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{edi_et_al:LIPIcs.TYPES.2015.6,
  author =	{Edi, Juan and Viso, Andr\'{e}s and Bonelli, Eduardo},
  title =	{{Efficient Type Checking for Path Polymorphism}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.6},
  URN =		{urn:nbn:de:0030-drops-84761},
  doi =		{10.4230/LIPIcs.TYPES.2015.6},
  annote =	{Keywords: lambda-calculus, pattern matching, path polymorphism, type checking}
}
  • Refine by Type
  • 6 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 2 2025
  • 1 2022
  • 1 2020
  • 1 2018

  • Refine by Author
  • 3 Kesner, Delia
  • 3 Viso, Andrés
  • 2 Bonelli, Eduardo
  • 1 Barenbaum, Pablo
  • 1 Chen, Zhuo Zoey
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Lambda calculus
  • 3 Theory of computation → Operational semantics
  • 2 Theory of computation → Linear logic
  • 1 Theory of computation
  • 1 Theory of computation → Equational logic and rewriting
  • Show More...

  • Refine by Keyword
  • 2 Call-by-Value
  • 1 Call-by-Name
  • 1 Call-by-Push-Value
  • 1 Evaluation strategies
  • 1 HOL
  • 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