**Formalising concurrent computation: CLF, Celf, and applications**

Presenter:
Sonia Marin
(IT-University of Copenhagen)

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)

This tutorial gives an introduction on how to implement an automated
theorem prover. Starting with the sequent calculus, we show how to
translate the axiom and the rules of the calculus step by step into
a Prolog program that can be used to automate proof search in the
sequent calculus.

After dealing with propositional logic, we extend this program step
by step in order to obtain a complete and sound theorem prover for
classical first-order logic. Afterwards, we show how these concepts
can be used to implement more efficient theorem provers based on
tableau and connection calculi.

The tutorial contains many examples to illustrate all of the presented
techniques. These techniques are general enough to implement any
(formal) proof calculus and can easily be adapted, e.g., to implement
a theorem prover based on a calculus for non-classical logics. A short
introduction into Prolog is given in the first part of this tutorial.