Parallel implementation models for the lambda-calculus using the geometry of interaction

An examination of Girard's execution formula suggests implementations of the Geometry of Interaction at the syntactic level. In this paper we limit our scope to ground-type terms and study the parallel aspects of such implementations, by introducing a family of machines which can be directly implemented. These machines address all the important implementation issues such as the choice of an inter-thread communication model, and allow to incorporate specific strategies for dividing the computation of the execution path into smaller tasks.Fundação Para a Ciência e a Tecnologia - PRAXIS XXI - BD/11261/97