Skip to Main content Skip to Navigation
New interface
Journal articles

The (In)Efficiency of interaction

Beniamino Accattoli 1 Ugo Dal Lago 2 Gabriele Vanoni 2 
1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce space efficiencies, the price being time performances often poorer than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how general this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types.
Document type :
Journal articles
Complete list of metadata
Contributor : Ugo Dal Lago Connect in order to contact the contributor
Submitted on : Friday, September 17, 2021 - 4:06:17 PM
Last modification on : Friday, July 8, 2022 - 10:04:12 AM


Files produced by the author(s)



Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The (In)Efficiency of interaction. Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.1-33. ⟨10.1145/3434332⟩. ⟨hal-03346750⟩



Record views


Files downloads