A Concurrent Logical Framework II: Examples and Applications

CLF is a new logical framework with 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 co...

Full description

Saved in:
Bibliographic Details
Main Authors: Cervesato, Iliano, Pfenning, Frank, Walker, David, Watkins, Kevin
Format: Report
Language:English
Subjects:
CALCULUS
CLF(CONCURRENT LOGICAL FRAMEWORK)
COMPUTER LOGIC
Computer Programming and Software
Computer Systems
CONCURRENCY
DATA PROCESSING SECURITY
DEDUCTIVE SYSTEMS
LLF(LINEAR LOGICAL FRAMEWORK)
PETRI NETS
PI CALCULUS
PROGRAMMING LANGUAGES
SYNTAX
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:CLF is a new logical framework with 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). In this report, the second of two technical reports describing CLF, we illustrate the expressive power of the framework by encoding several different concurrent languages including both the synchronous and asynchronous pi-calculus, an ML-like language with futures, lazy evaluation and concurrency primitives in the style of CML, Petri nets and finally, the security protocol specification language MSR. Throughout the report we assume the reader is already familiar with the formal definition of CLF. For detailed explanation and development of the type theory, please see A Concurrent Logical Framework I: Judgments and Properties WCPW02. Prepared in collaboration with the National Science Foundation under the title Meta-Logical Frameworks, grants CCR-9619584 and CCR-9988281.