TY - GEN
T1 - The useful MAM, a reasonable implementation of the strong λ-calculus
AU - Accattoli, Beniamino
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2016.
PY - 2016/1/1
Y1 - 2016/1/1
N2 - It has been a long-standing open problem whether the strong λ-calculus is a reasonable computational model, i.e. whether it can be implemented within a polynomial overhead with respect to the number of β-steps on models like Turing machines or RAM. Recently, Accattoli and Dal Lago solved the problem by means of a new form of sharing, called useful sharing, and realised via a calculus with explicit substitutions. This paper presents a new abstract machine for the strong λ-calculus based on useful sharing, the Useful Milner Abstract Machine, and proves that it reasonably implements leftmost-outermost evaluation. It provides both an alternative proof that the λ-calculus is reasonable and an improvement on the technology for implementing strong evaluation.
AB - It has been a long-standing open problem whether the strong λ-calculus is a reasonable computational model, i.e. whether it can be implemented within a polynomial overhead with respect to the number of β-steps on models like Turing machines or RAM. Recently, Accattoli and Dal Lago solved the problem by means of a new form of sharing, called useful sharing, and realised via a calculus with explicit substitutions. This paper presents a new abstract machine for the strong λ-calculus based on useful sharing, the Useful Milner Abstract Machine, and proves that it reasonably implements leftmost-outermost evaluation. It provides both an alternative proof that the λ-calculus is reasonable and an improvement on the technology for implementing strong evaluation.
U2 - 10.1007/978-3-662-52921-8_1
DO - 10.1007/978-3-662-52921-8_1
M3 - Conference contribution
AN - SCOPUS:84981516067
SN - 9783662529201
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 21
BT - Logic, Language, Information, and Computation - 23rd International Workshop, WoLLIC 2016, Proceedings
A2 - Väänänen, Jouko
A2 - Hirvonen, Åsa
A2 - de Queiroz, Ruy
PB - Springer Verlag
T2 - 23rd International Workshop on Logic, Language, Information, and Computation, WoLLIC 2016
Y2 - 16 August 2016 through 19 August 2016
ER -