Principal Typing for Parallel and non-Deterministic Lambda-calculus

Abstract

Parallelism and non-determinism are fundamental concepts in the process algebra theory. Combining them with lambda-calculus can enlighten the theory of higher-order process algebras. In recent papers an analysis of a lambda-calculus containing parallel and non-deterministic operators was carried on by means of a type assignment system with intersection and union types. The present paper answers the problem of determining principal types for this system.