This tutorial aims at introducing the Tableaux/FroCoS community to the Concurrent Logical Framework (CLF) and the Celf tool, as well as some of their applications.
A logical framework is a meta-language to specify and reason about deductive systems, as found in logic or programming language theory. The resulting specifications are executable and help reason about languages in a clear and simple way.
CLF is a logical framework for specifying and implementing concurrent systems. It is an extension of the LF framework with (i) linear types to support representation of stateful computation and (ii) a monad to support representation of concurrency. As a result, term equality in this language is not only defined modulo α-renaming but also modulo let-floating, which allows CLF signatures to be interpreted as concurrent logic programs.
Celf is an implementation of CLF, as Twelf is for LF. It allows the user to specify a concurrent system and provides them with type checking, type reconstruction and proof search. However, it does not yet include the meta-theoretic capabilities that Twelf has; this is under current investigation.
We will illustrate the CLF approach and the usage of Celf in a step-by-step manner by going
from a simple encoding of producer/consumer Petri nets to the more involved example of
the concurrent λ-calculus, showing how the various features of the framework combine
to allow clear formalisation of these concurrent systems.
Information on the content of this tutorial will be available soon.