Dexter Kozen (Cornell),
Kleene Algebra with Tests.
Kleene algebra with tests (KAT) is a versatile algebraic system for reasoning
about the equivalence of low-level imperative programs. It has been shown to
be useful in verifying compiler optimizations and performing static analysis.
This three-hour tutorial will introduce the basic definitions, results,
applications, and extensions of KAT. Possible topics include: basic examples
of equational reasoning; history and relation to classical systems such as
Hoare logic; common models, including language, relational, trace, and matrix
models; axiomatizations and their completeness and complexity; and
applications. If there is extra time, we will talk about the coalgebraic theory
and its use in modeling and reasoning about state-based systems.
Lawrence C. Paulson (Cambridge), The Isabelle/HOL Theorem Prover.
Isabelle/HOL is an interactive theorem prover for higher-order logic, with
powerful automation both to prove theorems and to find counterexamples. There
are two sophisticated user interfaces, and a flexible language in which to
express proofs. The tutorial will briefly cover two aspects of Isabelle usage:
(1) the verification of simple functional programs using induction and
simplification, and (2) inductively defined sets and relations.
Invited Talks
Peter O'Hearn (University College London), Algebraic Laws of Concurrency and Separation.
This talk reports on ongoing work -- with Tony Hoare, Akbar Hussain, Bernhard Möller,
Rasmus Petersen, Georg Struth, Ian Wehrman, and others-- drawing on
ideas from Kleene Algebra and Concurrent Separation Logic. The approach we are
taking abstracts from syntax or particular models. Message passing and shared
memory process interaction, and strong (interleaving) and weak (partial order)
approaches to sequencing, are accomodated as different models of the same core
algebraic axioms. The central structure is that of an ordered bimonoid, two
monotone monoids over the same poset representing parallel and sequential
composition, linked by an algebraic version of the exchange law from
2-categories. Rules of program logic, related to Hoare and Separation logics,
flow at once from this structure: one gets a generic program logic from the
algebra, which holds for a range of concrete models.
Damien Pous (CNRS Grenoble, France),
Using Relation Algebraic Methods in the Coq Proof Assistant.
If reasoning in a point-free algebraic setting can help on the paper,
it also greatly helps in a proof assistant.
We will present a Coq library for working with binary relations at the
algebraic, point-free, level.
By combining several automatic decision procedures (e.g., for Kleene
algebra and residuated semirings) and the higher-order features of
Coq, this library allows us to formalise various theorems in a very
simple way: we benefit from the expressiveness of an interactive
theorem prover and from the comfort of automation for decidable
fragments of relation algebra.
Alexander Krauss (Technical Univ. Munich),
Formalized Regular Expression Equivalence and Relation Algebra in
Isabelle.
We present the Isabelle formalization of an elegant equivalence checker
for regular expressions. It works by constructing a bisimulation
relation between (derivatives of) regular expressions. By mapping
expressions to binary relations, an automatic and complete proof method
for (in)equalities of binary relations over union, composition and
(reflexive) transitive closure is obtained, which adds a practically
useful decision procedure to the automation toolbox of Isabelle/HOL.
(Joint work with Tobias Nipkow.)
Winton Capital Management