A Concurrent Logical Framework I: Judgments and Properties

The Concurrent Logical Framework, or CLF, is a new logical framework in which concurrent computations can be represented as monadic objects, for which there is an intrinsic notion of concurrency. It is designed as a conservative extension of the linear logical framework LLF with the synchronous connectives (tensor), 1, !, and (\exists) of intuitionistic linear logic, encapsulated in a monad. LLF is itself a conservative extension of LF with the asynchronous connectives -o, & and T. The present report, the first of two technical reports describing CLF, presents the framework itself and its meta-theory. A novel, algorithmic formulation of the underlying type theory concentrating on canonical forms leads to a simple notion of definitional equality for concurrent computations in which the order of independent steps cannot be distinguished. The new formulation of the framework constitutes an original contribution even for the LF fragment. For many additional examples illustrating the use of the framework to specify and reason about object systems of interest, the reader is referred to the companion technical report on applications.