Embedding Display Calculi into Logical Frameworks

Jeremy Dawson & Rajeev Gore

Australian National University

Abstract

Logical frameworks are computer systems which allow a user to formalise
mathematics using specially designed languages based upon mathematical
logic.  They can be used to formalise rigorous proofs about logical
systems.  We compare several methods of implementing the display
(sequent) calculus \dRA\ for relation algebra in the logical frameworks
Isabelle and Twelf.  We aim for an implementation enabling us to
formalise, within the logical framework, proof-theoretic results such
as the cut-elimination theorem for \dRA\.  We discuss issues arising
from this requirement.

One style of implementation discussed permits the user to build a
proof, while a term recording the proof structure is created
automatically.  We have described how to adapt this style of proof to
the work of Fairtlough & Mendler in hardware design and verification.
They show how to describe a hardware component in Isabelle/HOL as
"timing details" : "abstract (logic) aspect".  We show how the user can
reason at the abstract (logical) level, while a term expressing timing
information is created automatically.

We then describe how the deep embedding of \dRA, using Isabelle/HOL,
was used to formalise a cut-elimination theorem for \dRA.  Our
implementation generalises easily to handle other display calculi.  We
also mention a published proof of strong normalization of
cut-elimination for Display Logic, and discuss the problems with it
which prevented us from being able to implement it, and required us to
produce a different proof.

Brief Bio:

Jeremy Dawson is currently (since Feb 2000)
a Senior Research Associate on the Large ARC
Grant "Proof Theoretical Implementations of Computer Science Logics",
working with Rajeev Gore.

Previously he has been with (inter alia)
  - Australia's Department of Defence on Computer Security for 9 years, and
  - CSIRO Mathematics and Statistics for 6 years, when his research was
in combinatorial mathematics (matroid theory).

He has a Ph.D. in combinatorial mathematics from the University of Sheffield.