Carnegie Mellon University
Browse

A Concurrent Logical Framework: The Propositional Fragment

Download (254.52 kB)
journal contribution
posted on 1979-01-01, 00:00 authored by Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker
We present the propositional fragment CLF0 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”.

History

Publisher Statement

All Rights Reserved

Date

1979-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC