posted on 1979-01-01, 00:00authored byKevin 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”.