48 citations · 142 across the 34 of their papers we have counts for
47 papers
Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
Beniamino Accattoli, Dan Ghica, Giulio Guerrieri +2
Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building closures pairing the transformed…
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…
Multi types and reasonable space
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambd…
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…
The (In)Efficiency of Interaction
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce efficiencies, the price being…
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…