A concurrent logical framework: The propositional fragment. (English) Zbl 1100.68548
Berardi, Stefano (ed.) et al., Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 – May 4, 2003. Revised selected papers. Berlin: Springer (ISBN 3-540-22164-6/pbk). Lecture Notes in Computer Science 3085, 355-377 (2004).
Summary: We present the propositional fragment CLF\(_0\) 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”.
For the entire collection see [Zbl 1052.68001].
For the entire collection see [Zbl 1052.68001].
MSC:
68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
03B70 | Logic in computer science |
68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |