Abstract

We propose a typed, higher-order, concurrent linear logic programming called higher-order ACL, which uniformly integrates a variety of mechanisms for concurrent computation based on asynchronous message passing. Higher-order ACL is based on a proof search paradigm according to the principle, proofs as computations, formulas as processes in linear logic. In higher-order ACL, processes as well as functions, and other values can be communicated via messages, which provides high modularity of concurrent programs. Higher-order ACL can be viewed as an asynchronous counterpart of Milner's higher-order, polyadic Pi-calculus. Moreover, higher-order ACL is equipped with an elegant ML-style type system that ensures (1) well typed programs can never cause type mismatch errors, and (2) there is a type inference algorithm which computes a most general typing for an untyped term. We also demonstrate a power of higher-order ACL by showing several examples of ``higher-order concurrent programming.''