Asynchronous communication model based on linear logic

Abstract

We propose a new framework called ACL for concurrent computation based on linear logic. ACL is a kind of linear logic programming framework, where its operational semantics is described in terms of proof construction in linear logic. We also give a model-theoretic semantics based on phase semantics, a model of linear logic. Our framework well captures concurrent computation based on asynchronous communication. It will, therefore, provide us with a new insight into other models of asynchronous concurrent computation from a logical point of view. We also expect ACL to become a formal framework for analysis, synthesis and transformation of concurrent programs by the use of techniques for traditional logic programming. ACL's attractive features for concurrent programming paradigms are also discussed. © 1995 BCS.