48 citations · 142 across the 34 of their papers we have counts for
37 papers · 1 filter
Positive Sharing and Abstract Machines
Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu
Wu's positive -calculus is a recent call-by-value -calculus with sharing coming from Miller and Wu's study of the proof-theoretical concept of focalization. Accattoli and Wu…
The Cost of Skeletal Call-by-Need, Smoothly
Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot +1
Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "s…
Positive Focusing is Directly Useful
Beniamino Accattoli, Jui-Hsuan Wu
Recently, Miller and Wu introduced the positive -calculus, a call-by-value -calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs…
The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
Beniamino Accattoli
Existing Curry-Howard interpretations of call-by-value evaluation for the -calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additiona…
Interaction Equivalence
Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto +1
Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence m…
IMELL Cut Elimination with Linear Overhead
Beniamino Accattoli, Claudio Sacerdoti Coen
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed…
Mirroring Call-by-Need, or Values Acting Silly
Beniamino Accattoli, Adrienne Lancelot
Call-by-need evaluation for the lambda-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 dupl…
Semantic Bound and Multi Types, Revisited
Beniamino Accattoli
Intersection types are a standard tool in operational and semantical studies of the lambda calculus. De Carvalho showed how multi types, a quantitative variant of intersection type…
A Diamond Machine For Strong Evaluation
Beniamino Accattoli, Pablo Barenbaum
Abstract machines for strong evaluation of the -calculus enter into arguments and have a set of transitions for backtracking out of an evaluated argument. We study a new abstrac…
Strong Call-by-Value and Multi Types
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the lambda-calculus. Recently, Accattoli et al. proposed a form of cal…
Normal Form Bisimulations By Value
Beniamino Accattoli, Adrienne Lancelot, Claudia Faggian
Normal form bisimilarities are a natural form of program equivalence resting on open terms, first introduced by Sangiorgi in call-by-name. The literature contains a normal form bis…
A Log-Sensitive Encoding of Turing Machines in the -Calculus
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
This note modifies the reference encoding of Turing machines in the -calculus by Dal Lago and Accattoli, which is tuned for time efficiency, as to accommodate logarithmic space.…
The Theory of Call-by-Value Solvability (long version)
Beniamino Accattoli, Giulio Guerrieri
The denotational semantics of the untyped lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different…
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
Beniamino Accattoli
This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials…
Reasonable Space for the -Calculus, Logarithmically
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Can the -calculus be considered a reasonable computational model? Can we use it for measuring the time space consumption of algorithms? While the literature conta…
Call-by-Value Solvability and Multi Types
Beniamino Accattoli, Giulio Guerrieri
This paper provides a characterization of call-by-value solvability using call-by-value multi types. Our work is based on Accattoli and Paolini's characterization of call-by-value…
Useful Open Call-by-Need
Beniamino Accattoli, Maico Leberle
This paper studies useful sharing, which is a sophisticated optimization for lambda-calculi, in the context of call-by-need evaluation in presence of open terms. Useful sharing tur…
The Space of Interaction (long version)
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
The space complexity of functional programs is not well understood. In particular, traditional implementation techniques are tailored to time efficiency, and space efficiency induc…
Semantic Bounds and Strong Call-by-Value Normalization
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
This paper explores two topics at once: the use of denotational semantics to bound the evaluation length of functional programs, and the semantics of strong (that is, possibly unde…
Strong Call-by-Value is Reasonable, Implosively
Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
Whether the number of beta-steps in the lambda-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate pro…
Factorize Factorization
Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization the…
Functional Pearl: The Distributive -Calculus
Beniamino Accattoli, Alejandro Díaz-Caro
We introduce a simple extension of the -calculus with pairs---called the distributive -calculus---obtained by adding a computational interpretation of the valid distributivit…
The Abstract Machinery of Interaction (Long Version)
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine,…
Factorization and Normalization, Essentially
Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as…