file.pdf (254.52 kB)
Download fileA Concurrent Logical Framework: The Propositional Fragment
journal contribution
posted on 1979-01-01, 00:00 authored by Kevin Watkins, Iliano Cervesato, Frank Pfenning, David WalkerWe 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”.