Call-by-Name and Call-by-Value as Token-Passing Interaction Nets

8 years 12 months ago
Call-by-Name and Call-by-Value as Token-Passing Interaction Nets
Two common misbeliefs about encodings of the λ-calculus in interaction nets (INs) are that they are good only for strategies that are not very well understood (e.g. optimal reduction) and that they always have to deal in a complex way with boxes. In brief, the theory of interaction nets is more or less disconnected from the standard theory: we can do things in INs that we cannot do with terms, which is true [5, 10]; and we cannot do in INs things that can easily be done with terms. This paper contributes to fighting this misbelief by showing that the standard call-by-name and call-by-value strategies of the λ-calculus are encoded in interaction nets in a very simple and extensible way, and in particular that these encodings do not need any notion of box. This work can also be seen as a first step towards a generic approach to derive graph-based machines.
François-Régis Sinot
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors François-Régis Sinot
Comments (0)