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.''