6 Search Results for "Díaz-Caro, Alejandro"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.28
Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic

Authors: Alejandro Díaz-Caro and Octavio Malherbe

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
Traditional approaches to modelling parallelism and algebraic structure in lambda calculi often rely on monads - as in Moggi’s framework - or on rich categorical structures such as biproducts - as used in certain models of linear logic. In this work, we propose a minimal alternative that captures both parallelism and weighted parallelism (linear combinations) within the setting of intuitionistic propositional logic, without resorting to monads or assuming the existence of biproducts. We introduce two lambda calculi: a parallel lambda calculus and an algebraic lambda calculus, both extending full propositional intuitionistic logic. Their semantics are given in two categories: Mag_{Set}, whose objects are magmas and arrows are functions in Set; and AMag^{𝒮}_{Set}, whose objects are action magmas. The key technical challenge addressed is the interpretation of disjunction in the presence of parallel and algebraic operators. Since the usual coproduct structure is unavailable in our minimal setting, we propose a novel set-theoretic interpretation based on the union of the disjoint union and the Cartesian product. This allows for the construction of sound and adequate models for both calculi. Our results offer a unified and structurally lightweight framework for modelling parallelism and algebraic effects in intuitionistic logic, opening the way to alternatives beyond the traditional monadic or linear logic approaches.
Cite as

Alejandro Díaz-Caro and Octavio Malherbe. Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{diazcaro_et_al:LIPIcs.FSTTCS.2025.28,
  author =	{D{\'\i}az-Caro, Alejandro and Malherbe, Octavio},
  title =	{{Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.28},
  URN =		{urn:nbn:de:0030-drops-251098},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.28},
  annote =	{Keywords: Algebraic lambda calculus, Categorical semantics, Disjunction, Proof theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.22
Branch Sequentialization in Quantum Polytime

Authors: Emmanuel Hainry, Romain Péchoux, and Mário Silva

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

Abstract
Quantum algorithms leverage the use of quantumly-controlled data in order to achieve computational advantage. This implies that the programs use constructs depending on quantum data and not just classical data such as measurement outcomes. Current compilation strategies for quantum control flow involve compiling the branches of a quantum conditional, either in-depth or in-width, which in general leads to circuits of exponential size. This problem is coined as the branch sequentialization problem. We introduce and study a compilation technique for avoiding branch sequentialization on a language that is sound and complete for quantum polynomial time, thus, improving on existing polynomial-size-preserving compilation techniques.
Cite as

Emmanuel Hainry, Romain Péchoux, and Mário Silva. Branch Sequentialization in Quantum Polytime. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hainry_et_al:LIPIcs.FSCD.2025.22,
  author =	{Hainry, Emmanuel and P\'{e}choux, Romain and Silva, M\'{a}rio},
  title =	{{Branch Sequentialization in Quantum Polytime}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{22:1--22:22},
  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.22},
  URN =		{urn:nbn:de:0030-drops-236373},
  doi =		{10.4230/LIPIcs.FSCD.2025.22},
  annote =	{Keywords: Quantum Programs, Implicit Computational Complexity, Quantum Circuits}
}
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.FSCD.2023.11
Two Decreasing Measures for Simply Typed λ-Terms

Authors: Pablo Barenbaum and Cristian Sottile

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

Abstract
This paper defines two decreasing measures for terms of the simply typed λ-calculus, called the 𝒲-measure and the 𝒯^{𝐦}-measure. A decreasing measure is a function that maps each typable λ-term to an element of a well-founded ordering, in such a way that contracting any β-redex decreases the value of the function, entailing strong normalization. Both measures are defined constructively, relying on an auxiliary calculus, a non-erasing variant of the λ-calculus. In this system, dubbed the λ^{𝐦}-calculus, each β-step creates a "wrapper" containing a copy of the argument that cannot be erased and cannot interact with the context in any other way. Both measures rely crucially on the observation, known to Turing and Prawitz, that contracting a redex cannot create redexes of higher degree, where the degree of a redex is defined as the height of the type of its λ-abstraction. The 𝒲-measure maps each λ-term to a natural number, and it is obtained by evaluating the term in the λ^{𝐦}-calculus and counting the number of remaining wrappers. The 𝒯^{𝐦}-measure maps each λ-term to a structure of nested multisets, where the nesting depth is proportional to the maximum redex degree.
Cite as

Pablo Barenbaum and Cristian Sottile. Two Decreasing Measures for Simply Typed λ-Terms. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.FSCD.2023.11,
  author =	{Barenbaum, Pablo and Sottile, Cristian},
  title =	{{Two Decreasing Measures for Simply Typed \lambda-Terms}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{11:1--11:19},
  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.11},
  URN =		{urn:nbn:de:0030-drops-179956},
  doi =		{10.4230/LIPIcs.FSCD.2023.11},
  annote =	{Keywords: Lambda Calculus, Rewriting, Termination, Strong Normalization, Simple Types}
}
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.FSCD.2019.14
Proof Normalisation in a Logic Identifying Isomorphic Propositions

Authors: Alejandro Díaz-Caro and Gilles Dowek

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We define a fragment of propositional logic where isomorphic propositions, such as A wedge B and B wedge A, or A ==> (B wedge C) and (A ==> B) wedge (A ==> C) are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.
Cite as

Alejandro Díaz-Caro and Gilles Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2019.14,
  author =	{D{\'\i}az-Caro, Alejandro and Dowek, Gilles},
  title =	{{Proof Normalisation in a Logic Identifying Isomorphic Propositions}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.14},
  URN =		{urn:nbn:de:0030-drops-105210},
  doi =		{10.4230/LIPIcs.FSCD.2019.14},
  annote =	{Keywords: Simply typed lambda calculus, Isomorphisms, Logic, Cut-elimination, Proof-reduction}
}
  • Refine by Type
  • 6 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2023
  • 1 2022
  • 1 2019

  • Refine by Author
  • 3 Díaz-Caro, Alejandro
  • 2 Dowek, Gilles
  • 1 Barenbaum, Pablo
  • 1 Faggian, Claudia
  • 1 Hainry, Emmanuel
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Proof theory
  • 2 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Lambda calculus
  • 2 Theory of computation → Linear logic
  • 2 Theory of computation → Quantum computation theory
  • Show More...

  • Refine by Keyword
  • 2 Proof theory
  • 1 Algebraic lambda calculus
  • 1 Categorical semantics
  • 1 Cut-elimination
  • 1 Disjunction
  • 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