Abstract

Geometry of interaction was introduced by Girard, as a semantics of computation which expresses the dynamics of computation by more mathematical means than syntactical rewriting.

I present - more or less from scratch - a "computational device" derived from the geometry of interaction, specifically designed in view of the optimal, parallel and effective execution of functional programs.

- Optimality is obtained by means of a graph reduction technique, namely directed virtual reduction, that is restriction of the virtual reduction studied by Danos & Regnier.

- Effectiveness is obtained by the embedding to directed virtual nets of the notion of safe operators introduced by Asperti.

- Fine granularity of the distributed implementation is controlled by means of an adhoc message aggregation technique.