Search Results

Documents authored by Accattoli, Beniamino

Document
DOI: 10.4230/LIPIcs.FSCD.2024.23
Mirroring Call-By-Need, or Values Acting Silly

Authors: Beniamino Accattoli and Adrienne Lancelot

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Call-by-need evaluation for the λ-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need - that is, its operational equivalence with call-by-name - showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
Cite as

Beniamino Accattoli and Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.23,
  author =	{Accattoli, Beniamino and Lancelot, Adrienne},
  title =	{{Mirroring Call-By-Need, or Values Acting Silly}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.23},
  URN =		{urn:nbn:de:0030-drops-203527},
  doi =		{10.4230/LIPIcs.FSCD.2024.23},
  annote =	{Keywords: Lambda calculus, intersection types, call-by-value, call-by-need}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.24
IMELL Cut Elimination with Linear Overhead

Authors: Beniamino Accattoli and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for ESC/IMELL, and the first such one. Here, we refine Accattoli’s result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.
Cite as

Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24,
  author =	{Accattoli, Beniamino and Sacerdoti Coen, Claudio},
  title =	{{IMELL Cut Elimination with Linear Overhead}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.24},
  URN =		{urn:nbn:de:0030-drops-203539},
  doi =		{10.4230/LIPIcs.FSCD.2024.24},
  annote =	{Keywords: Lambda calculus, linear logic, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.7
Semantic Bounds and Multi Types, Revisited

Authors: Beniamino Accattoli

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Intersection types are a standard tool in operational and semantical studies of the λ-calculus. De Carvalho showed how multi types, a quantitative variant of intersection types providing a handy presentation of the relational denotational model, allows one to extract precise bounds on the number of β-steps and the size of normal forms. In the last few years, de Carvalho’s work has been extended and adapted to a number of λ-calculi, evaluation strategies, and abstract machines. These works, however, only adapt the first part of his work, that extracts bounds from multi type derivations, while never consider the second part, which deals with extracting bounds from the multi types themselves. The reason is that this second part is more technical, and requires to reason up to type substitutions. It is however also the most interesting, because it shows that the bounding power is inherent to the relational model (which is induced by the types, without the derivations), independently of its presentation as a type system. Here we dissect and clarify the second part of de Carvalho’s work, establishing a link with principal multi types, and isolating a key property independent of type substitutions.
Cite as

Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.CSL.2024.7,
  author =	{Accattoli, Beniamino},
  title =	{{Semantic Bounds and Multi Types, Revisited}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{7:1--7:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.7},
  URN =		{urn:nbn:de:0030-drops-196504},
  doi =		{10.4230/LIPIcs.CSL.2024.7},
  annote =	{Keywords: Lambda calculus, intersection types, denotational semantics, linear logic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.5
Formalizing Functions as Processes

Authors: Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
We present the first formalization of Milner’s classic translation of the λ-calculus into the π-calculus. It is a challenging result with respect to variables, names, and binders, as it requires one to relate variables and binders of the λ-calculus with names and binders in the π-calculus. We formalize it in Abella, merging the set of variables and the set of names, thus circumventing the challenge and obtaining a neat formalization. About the translation, we follow Accattoli’s factoring of Milner’s result via the linear substitution calculus, which is a λ-calculus with explicit substitutions and contextual rewriting rules, mediating between the λ-calculus and the π-calculus. Another aim of the formalization is to investigate to which extent the use of contexts in Accattoli’s refinement can be formalized.
Cite as

Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen. Formalizing Functions as Processes. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.ITP.2023.5,
  author =	{Accattoli, Beniamino and Blanc, Horace and Sacerdoti Coen, Claudio},
  title =	{{Formalizing Functions as Processes}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{5:1--5:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.5},
  URN =		{urn:nbn:de:0030-drops-183800},
  doi =		{10.4230/LIPIcs.ITP.2023.5},
  annote =	{Keywords: Lambda calculus, pi calculus, proof assistants, binders, Abella}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.4
Useful Open Call-By-Need

Authors: Beniamino Accattoli and Maico Leberle

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

Abstract
This paper studies useful sharing, which is a sophisticated optimization for λ-calculi, in the context of call-by-need evaluation in presence of open terms. Useful sharing turns out to be harder in call-by-need than in call-by-name or call-by-value, because call-by-need evaluates inside environments, making it harder to specify when a substitution step is useful. We isolate the key involved concepts and prove the correctness and the completeness of useful sharing in this setting.
Cite as

Beniamino Accattoli and Maico Leberle. Useful Open Call-By-Need. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.CSL.2022.4,
  author =	{Accattoli, Beniamino and Leberle, Maico},
  title =	{{Useful Open Call-By-Need}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{4:1--4:21},
  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.4},
  URN =		{urn:nbn:de:0030-drops-157242},
  doi =		{10.4230/LIPIcs.CSL.2022.4},
  annote =	{Keywords: lambda calculus, call-by-need, operational semantics, sharing, cost models}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.6
Factorize Factorization

Authors: Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri

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

Abstract
We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our approach is well adapted to deal with extensions of the call-by-name and call-by-value λ-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with β-reduction. We then closely analyze some common factorization schemas for the λ-calculus. Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno’s non-deterministic λ-calculus and - for call-by-value - Carraro and Guerrieri’s shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
Cite as

Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorize Factorization. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.CSL.2021.6,
  author =	{Accattoli, Beniamino and Faggian, Claudia and Guerrieri, Giulio},
  title =	{{Factorize Factorization}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{6:1--6:25},
  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.6},
  URN =		{urn:nbn:de:0030-drops-134407},
  doi =		{10.4230/LIPIcs.CSL.2021.6},
  annote =	{Keywords: Lambda Calculus, Rewriting, Reduction Strategies, Factorization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2019.1
A Fresh Look at the lambda-Calculus (Invited Talk)

Authors: Beniamino Accattoli

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

Abstract
The (untyped) lambda-calculus is almost 90 years old. And yet - we argue here - its study is far from being over. The paper is a bird’s eye view of the questions the author worked on in the last few years: how to measure the complexity of lambda-terms, how to decompose their evaluation, how to implement it, and how all this varies according to the evaluation strategy. The paper aims at inducing a new way of looking at an old topic, focussing on high-level issues and perspectives.
Cite as

Beniamino Accattoli. A Fresh Look at the lambda-Calculus (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.FSCD.2019.1,
  author =	{Accattoli, Beniamino},
  title =	{{A Fresh Look at the lambda-Calculus}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{1:1--1:20},
  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.1},
  URN =		{urn:nbn:de:0030-drops-105083},
  doi =		{10.4230/LIPIcs.FSCD.2019.1},
  annote =	{Keywords: lambda-calculus, sharing, abstract machines, type systems, rewriting}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.39
Linear Logic and Strong Normalization

Authors: Beniamino Accattoli

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
Strong normalization for linear logic requires elaborated rewriting techniques. In this paper we give a new presentation of MELL proof nets, without any commutative cut-elimination rule. We show how this feature induces a compact and simple proof of strong normalization, via reducibility candidates. It is the first proof of strong normalization for MELL which does not rely on any form of confluence, and so it smoothly scales up to full linear logic. Moreover, it is an axiomatic proof, as more generally it holds for every set of rewriting rules satisfying three very natural requirements with respect to substitution, commutation with promotion, full composition, and Kesner's IE property. The insight indeed comes from the theory of explicit substitutions, and from looking at the exponentials as a substitution device.
Cite as

Beniamino Accattoli. Linear Logic and Strong Normalization. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 39-54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.RTA.2013.39,
  author =	{Accattoli, Beniamino},
  title =	{{Linear Logic and Strong Normalization}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{39--54},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{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.RTA.2013.39},
  URN =		{urn:nbn:de:0030-drops-40515},
  doi =		{10.4230/LIPIcs.RTA.2013.39},
  annote =	{Keywords: linear logic, proof nets, strong normalization, explicit substitutions}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.6
An Abstract Factorization Theorem for Explicit Substitutions

Authors: Beniamino Accattoli

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
We study a simple form of standardization, here called factorization, for explicit substitutions calculi, i.e. lambda-calculi where beta-reduction is decomposed in various rules. These calculi, despite being non-terminating and non-orthogonal, have a key feature: each rule terminates when considered separately. It is well-known that the study of rewriting properties simplifies in presence of termination (e.g. confluence reduces to local confluence). This remark is exploited to develop an abstract theorem deducing factorization from some axioms on local diagrams. The axioms are simple and easy to check, in particular they do not mention residuals. The abstract theorem is then applied to some explicit substitution calculi related to Proof-Nets. We show how to recover standardization by levels, we model both call-by-name and call-by-value calculi and we characterize linear head reduction via a factorization theorem for a linear calculus of substitutions.
Cite as

Beniamino Accattoli. An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 6-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.RTA.2012.6,
  author =	{Accattoli, Beniamino},
  title =	{{An Abstract Factorization Theorem for Explicit Substitutions}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{6--21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.6},
  URN =		{urn:nbn:de:0030-drops-34813},
  doi =		{10.4230/LIPIcs.RTA.2012.6},
  annote =	{Keywords: lambda-calculus, Standardization, Explicit Substitutions, Abstract rewriting, Diagrammatic reasoning}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.22
On the Invariance of the Unitary Cost Model for Head Reduction

Authors: Beniamino Accattoli and Ugo Dal Lago

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
The lambda-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. In this paper, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the lambda-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies the unitary cost model is invariant, if any.
Cite as

Beniamino Accattoli and Ugo Dal Lago. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 22-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.RTA.2012.22,
  author =	{Accattoli, Beniamino and Dal Lago, Ugo},
  title =	{{On the Invariance of the Unitary Cost Model for Head Reduction}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{22--37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.22},
  URN =		{urn:nbn:de:0030-drops-34820},
  doi =		{10.4230/LIPIcs.RTA.2012.22},
  annote =	{Keywords: lambda calculus, cost models, explicit substitutions, implicit computational complexity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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