48 citations · 142 across the 34 of their papers we have counts for
10 papers · 1 filter
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…
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…
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…
Tight Typings and Split Bounds
Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
Multi types---aka non-idempotent intersection types---have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the…
The Maximal MAM, a Reasonable Implementation of the Maximal Strategy
Beniamino Accattoli
This note is about a reasonable abstract machine, called Maximal MAM, implementing the maximal strategy of the lambda-calculus, that is, the strategy that always produces a longest…
The Complexity of Abstract Machines
Beniamino Accattoli
The lambda-calculus is a peculiar computational model whose definition does not come with a notion of machine. Unsurprisingly, implementations of the lambda-calculus have been stud…
(Leftmost-Outermost) Beta Reduction is Invariant, Indeed
Beniamino Accattoli, Ugo Dal Lago
Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machi…
A Strong Distillery
Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
Abstract machines for the strong evaluation of lambda-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants…
Distilling Abstract Machines (Long Version)
Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear…
Evaluating functions as processes
Beniamino Accattoli
A famous result by Milner is that the lambda-calculus can be simulated inside the pi-calculus. This simulation, however, holds only modulo strong bisimilarity on processes, i.e. th…