4 papers
On Jumps, Interactions, and Intersection Types
Stefano Catozi, Ugo Dal Lago, Gabriele Vanoni
The Jumping Abstract Machine (JAM), an evaluation mechanism for the -calculus, was introduced by Danos and Regnier as an optimization of the Interaction Abstract Machine (IAM),…
Multi types and reasonable space
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambd…
Slightly Non-Linear Higher-Order Tree Transducers
Lê Thà nh Dũng Nguyên, Gabriele Vanoni
We investigate the tree-to-tree functions computed by "affine -transducers": tree automata whose memory consists of an affine -term instead of a finite state. They can be s…
Interaction Equivalence
Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto +1
Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence m…