TY - GEN
T1 - The machinery of interaction
AU - Accattoli, Beniamino
AU - Dal Lago, Ugo
AU - Vanoni, Gabriele
N1 - Publisher Copyright:
© 2020 Owner/Author.
PY - 2020/9/8
Y1 - 2020/9/8
N2 - This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear logic proof nets, and whose soundness proof is convoluted and passes through various other formalisms. Here we provide a new direct proof of its correctness, based on a variant of Sands's improvements, a natural notion of bisimulation. Moreover, our proof is carried out on a new presentation of the IAM, defined as a machine acting directly on λ-terms, rather than on linear logic proof nets.
AB - This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear logic proof nets, and whose soundness proof is convoluted and passes through various other formalisms. Here we provide a new direct proof of its correctness, based on a variant of Sands's improvements, a natural notion of bisimulation. Moreover, our proof is carried out on a new presentation of the IAM, defined as a machine acting directly on λ-terms, rather than on linear logic proof nets.
KW - abstract machines
KW - geometry of interaction
KW - lambda-calculus
U2 - 10.1145/3414080.3414108
DO - 10.1145/3414080.3414108
M3 - Conference contribution
AN - SCOPUS:85092783444
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP 2020 - Part of BOPL 2020 - Bologna Federated Conference on Programming Languages 2020
PB - Association for Computing Machinery
T2 - 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP 2020 - Part of 2020 Bologna Federated Conference on Programming Languages, BOPL 2020
Y2 - 8 September 2020 through 10 September 2020
ER -