FroCoS/TABLEAUX Tutorials

Formalising concurrent computation: CLF, Celf, and applications

Presenters: Sonia Marin (IT-University of Copenhagen), Giselle Reis (Carnegie Mellon University in Qatar) and Iliano Cervesato (Carnegie Mellon University).

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.

How to Build an Automated Theorem Prover - An Introductory Tutorial (invited TABLEAUX tutorial)

Presenter: Jens Otten (University of Oslo)

Information on the content of this tutorial will be available soon.