4 Search Results for "Carraro, Alberto"

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.MFCS.2021.13
(Un)Decidability for History Preserving True Concurrent Logics

Authors: Paolo Baldan, Alberto Carraro, and Tommaso Padoan

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We investigate the satisfiability problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal (in)dependencies. Variants of such logics have been studied, with different expressiveness, corresponding to a number of true concurrent behavioural equivalences. Here we focus on a mu-calculus style logic that represents the counterpart of history-preserving (hp-)bisimilarity, a typical equivalence in the true concurrent spectrum of bisimilarities. It is known that one can decide whether or not two 1-safe Petri nets (and in general finite asynchronous transition systems) are hp-bisimilar. Moreover, for the logic that captures hp-bisimilarity the model-checking problem is decidable with respect to prime event structures satisfying suitable regularity conditions. To the best of our knowledge, the problem of satisfiability has been scarcely investigated in the realm of true concurrent logics. We show that satisfiability for the logic for hp-bisimilarity is undecidable via a reduction from domino tilings. The fragment of the logic without fixpoints, instead, turns out to be decidable. We consider these results a first step towards a more complete investigation of the satisfiability problem for true concurrent logics, which we believe to have notable solvable cases.
Cite as

Paolo Baldan, Alberto Carraro, and Tommaso Padoan. (Un)Decidability for History Preserving True Concurrent Logics. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.MFCS.2021.13,
  author =	{Baldan, Paolo and Carraro, Alberto and Padoan, Tommaso},
  title =	{{(Un)Decidability for History Preserving True Concurrent Logics}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.13},
  URN =		{urn:nbn:de:0030-drops-144532},
  doi =		{10.4230/LIPIcs.MFCS.2021.13},
  annote =	{Keywords: Event structures, history-preserving bisimilarity, true concurrent behavioural logics, satisfiability, decidability, domino systems}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.152
On the equational consistency of order-theoretic models of the lambda-calculus

Authors: Alberto Carraro and Antonino Salibra

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of lambda calculus.
Cite as

Alberto Carraro and Antonino Salibra. On the equational consistency of order-theoretic models of the lambda-calculus. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 152-166, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{carraro_et_al:LIPIcs.CSL.2012.152,
  author =	{Carraro, Alberto and Salibra, Antonino},
  title =	{{On the equational consistency of order-theoretic models of the lambda-calculus}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{152--166},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.152},
  URN =		{urn:nbn:de:0030-drops-36703},
  doi =		{10.4230/LIPIcs.CSL.2012.152},
  annote =	{Keywords: Lambda calculus, order-incompleteness, partially ordered models}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.97
Full Abstraction for Resource Calculus with Tests

Authors: Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We study the semantics of a resource sensitive extension of the lambda-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D infinity model of the pure lambda-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a ``must'' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula.
Cite as

Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full Abstraction for Resource Calculus with Tests. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 97-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bucciarelli_et_al:LIPIcs.CSL.2011.97,
  author =	{Bucciarelli, Antonio and Carraro, Alberto and Ehrhard, Thomas and Manzonetto, Giulio},
  title =	{{Full Abstraction for Resource Calculus with Tests}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{97--111},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.97},
  URN =		{urn:nbn:de:0030-drops-32250},
  doi =		{10.4230/LIPIcs.CSL.2011.97},
  annote =	{Keywords: resource lambda calculus, relational semantics, full abstraction, differential linear logic}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2021
  • 1 2012
  • 1 2011

  • Refine by Author
  • 3 Carraro, Alberto
  • 2 Manzonetto, Giulio
  • 1 Baldan, Paolo
  • 1 Bucciarelli, Antonio
  • 1 Cerda, Rémy
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Rewrite systems

  • Refine by Keyword
  • 1 Böhm trees
  • 1 Event structures
  • 1 Lambda calculus
  • 1 Ohana trees
  • 1 Taylor expansion
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact