A Concurrent Logical Framework I: Judgments and Properties
Abstract
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 (circle multiply, 1, !, and there exists) of intuitionistic linear logic, encapsulated in a monad. LLF is itself a conservative extension of LF with the asynchronous connectives (logical negation, & and T). The present report, the first of two technical reports describing CLF, presents the frame- work itself and its metatheory. 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 CPWW02.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 2003
- Accession Number
- ADA418517
Entities
People
- David Walker
- Frank Pfenning
- Iliano Cervesato
- Kevin Watkins
Organizations
- Carnegie Mellon University