A Current Logical Framework: The Propositional Fragment

We present the propositional fragment CLF of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations in an object language. The underlying type theory uses monadic types to segregate values from computations. Thi...

Full description

Saved in:
Bibliographic Details
Main Authors: Watkins, Kevin, Cervesato, Iliano, Pfenning, Frank, Walker, David
Format: Report
Language:English
Subjects:
CLF(CONCURRENT LOGICAL FRAMEWORK)
COMPUTER LOGIC
COMPUTER PROGRAMMING
Computer Programming and Software
LINEAR PROGRAMMING
PROGRAMMING LANGUAGES
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present the propositional fragment CLF of the Concurrent Logical Framework (CLF). CLF extends the Linear Logical Framework to allow the natural representation of concurrent computations in an object language. The underlying type theory uses monadic types to segregate values from computations. This separation leads to a tractable notion of definitional equality that identifies computations differing only in the order of execution of independent steps. From a logical point of view our type theory can be seen as a novel combination of lax logic and dual intuitionistic linear logic. An encoding of a small Petri net exemplifies the representation methodology, which can be summarized as concurrent computations as monadic expressions. Prepared in cooperation with Princeton University, Department of Computer Science, Princeton, NJ.