Beniamino Accattoli

The Complexity of Abstract Machines

Abstract:

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 studied for decades.

Abstract machines are implementations schema for fixed evaluation strategies that are a compromise between theory and practice: they are concrete enough to provide a notion of machine and abstract enough to avoid the many intricacies of actual implementations.

There is an extensive literature about abstract machines for the lambda-calculus, and yet — quite mysteriously — the efficiency of these machines with respect to the strategy that they implement has almost never been studied.

In this talk I will provide an unusual introduction to abstract machines, based on the complexity of their overhead with respect to the length of the implemented strategies. I will compare different approaches, optimizations, and evaluation strategies, providing a new modular and uniform perspective on abstract machines.

The results I will discuss are based on a series of recent works in collaboration with Pablo Barenbaum, Ugo Dal Lago, Giulio Guerrieri, Damiano Mazza, and Claudio Sacerdoti Coen.