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

Full description

Saved in:
Bibliographic Details
Main Authors: Watkins, Kevin, Cervesato, Iliano, Pfenning, Frank, Walker, David
Format: Report
Language:English
Subjects:
ALGORITHMS
COMPUTATIONS
Computer Hardware
COMPUTER LOGIC
CONCURRENCY
FORMULATIONS
LINEAR LOGIC
LINEAR PROGRAMMING
LOGICAL FRAMEWORKS
TYPE THEORY
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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. Prepared in collaboration with the National Science Foundation under the title Meta-Logical Frameworks, grants CCR-9619584 and CCR-9988281.