Thursday 5 October 2017, 14:00, LSV library: Environments and the Complexity of Abstract Machines, Bruno Barras (Inria).

Joint work with Beniamino Accattoli.

This talk deals with the complexity of a large family of interpreters of the lambda-calculus (aka abstract machines). The main criterion for a classification of such machines is the strategy it implements. Here we consider the Call-by-Name, Call-by-Value and Call-by-Need strategies. The goal is not to compare strategies but rather how efficiently they can be implemented.

Most abstract machines introduce the notion of environment (aka substitution), but we typically distinguish two main styles. On the one hand, machines with global environments have only one such environment that apply to all terms. On the other hand, in the local environment style, each term has his own environment.

Finally, the datatypes used for environments and terms may also have an impact on the efficiency of abstract machines.

We make a uniform complexity analysis that applies to all sensible combinations of the aforementioned parameters. It suggests that the complexity can be improved by a third style that we called split environments. They have already been introduced by Sestoft for the Call-by-Value, but we remark as a general fact that they can be considered as the best of both worlds.

The second part of the talk will extend these results to the lambda-calculus with concrete datatypes and pattern-matching.