\documentclass{entcs} % entcs ignores point size %\usepackage{makeidx} %\usepackage{acmnew-xref} \usepackage{latexsym} \usepackage{amssymb} %\usepackage{exptrees} \renewcommand{\today}{\number\day\ \ifcase\month\or January\or February\or March\or April\or May\or June\or July\or August\or September\or October\or November\or December\fi \ \number\year} %\setlength \parskip {1.0ex} \setcounter{secnumdepth}2 \setcounter{tocdepth}2 % \pagestyle{myheadings} \newcommand\comment[1]{} \date{\today} \newcommand\cfile{} %\renewcommand{\thepage}{\roman{page}} \newcommand\shrinklist[1]{ \setlength\parskip{#1\parskip} \setlength\itemsep{#1\itemsep} \setlength\itemindent{#1\itemindent} \setlength\topsep{#1\topsep} } \newcommand\invrule[2]{ % for use in non-math mode, args interpreted in math mode \begin{tabular}{@{}c@{}} $ #1 $ \\ \hline \hline $ #2 $ \end{tabular}} \newcommand\slrule[2]{ % similar to \frac, except % for use in non-math mode, args interpreted in math mode \begin{tabular}{@{}c@{}} $ #1 $ \\ \hline $ #2 $ \end{tabular}} %\newcommand\proof{\noindent\textbf{Proof.}} \newcommand\src[1]{source file \texttt{#1}} \newcommand\apsrc[1]{Appendix \ref{app:code}} %\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})} \newcommand\seesrc[1]{(see source file \texttt{#1})} %\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})} \newcommand\insrc[1]{in source file \texttt{#1}} \newcommand\page[1]{page~\pageref{#1}} \newcommand\fig[1]{Fig.~\ref{fig:#1}} \newcommand\ch[1]{Chapter~\ref{ch:#1}} \newcommand\tbl[1]{Table~\ref{tbl:#1}} \newcommand\thrm[1]{Theorem~\ref{thrm:#1}} %\newcommand\lem[1]{Lemma~\ref{lem:#1}} \newcommand\ttl[1]{\tti{#1}\label{#1}} \newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}} \newcommand\ttdef[1]{\texttt{#1}\tti{#1}} \newcommand\tti[1]{\index{#1@\texttt{#1}}} \newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}} \newcommand\dRA{{\boldmath $\delta$}\textbf{RA}} \newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}} \newcommand\NRA{\textbf{NRA}} \newcommand\RA{\textbf{RA}} %\newcommand\M{$\mathcal M$} \newcommand\M{\ensuremath{\mathcal M}} \newcommand\Mp{$\mathcal M'$} \newcommand\up[1]{\vspace{-#1ex}} \newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree \newcommand\1{\textbf 1} \newcommand\0{\textbf 0} % automatically defined in LLNCS style %\newtheorem{thm}{Theorem}%[chapter] %\newtheorem{lemma}[thm]{Lemma} %\newtheorem{defn}[thm]{Definition} %\newtheorem{cor}{Corollary}[thm] %\renewcommand\thecor{\thethm(\arabic{cor})} \pagestyle{plain} \raggedbottom \begin{document} \begin{frontmatter} \title{Embedding Display Calculi into Logical Frameworks : Comparing Twelf and Isabelle} \author{Jeremy E. Dawson\thanksref{smallgrant}}, \address{ Department of Computer Science, Faculty of Engineering and Information Technology, Australian National University} \thanks[smallgrant]{Supported by an Australian Research Council Small Research Grant.} \author{Rajeev Gor\'e\thanksref{qeII}}, \address{ Automated Reasoning Group, Computer Sciences Laboratory, Research School of Information Science and Engineering, Australian National University \\ and \\ Department of Computer Science, Faculty of Engineering and Information Technology, Australian National University} \thanks[qeII]{Supported by an Australian Research Council Queen Elizabeth II Fellowship.} \begin{abstract} Logical frameworks are computer systems which allow a user to formalise mathematics using specially designed languages based upon mathematical logic and Church's theory of types. They can be used to derive programs from logical specifications, thereby guaranteeing the correctness of the resulting programs. They can also 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\, and any associated increase in proof length. We discuss issues arising from this requirement. % %We then show how the implementation can be used to prove results comparing %alternative formalisations of relation algebra %from a proof-theoretic perspective. \end{abstract} \begin{keyword} logical frameworks, higher-order logics, proof systems for relation algebra, non-classical logics, automated deduction, display logic. \end{keyword} \end{frontmatter} \sloppy %\newpage %% Here begins the main text \section{Introduction and Motivation} \label{intro} Logical frameworks are computer systems which allow a user to formalise mathematics using specially designed languages based upon mathematical logic and Church's theory of types. They can be used to derive programs from logical specifications, thereby guaranteeing the correctness of the resulting programs. They can also be used to formalise rigorous proofs about logical systems. Relation algebras \cite{maddux-introductory} are extensions of Boolean algebras; whereas Boolean algebras model subsets of a given set, relation algebras model binary relations on a given set. Relation algebras have operations such as relational composition and relational converse, and Boolean operations such as intersection (conjunction) and complement (negation). Relation algebras form the basis of relational databases \cite{elmasri-navathe-database} and of the specification and proof of correctness of programs, particularly in the style of Mili \cite{mili-relational}. Display Logic \cite{belnap-display} is a generalised sequent framework for non-classical logics, based on the Gentzen sequent calculus \cite{gallier-logic}. %It can be applied to give syntactic proof systems for various logics. Its advantages include a generic cut-elimination theorem, which applies whenever the rules for the display calculus satisfy certain, easily checked, conditions. It is an extremely general logical formalism, applicable to many (classical and non-classical) logics in a uniform way \cite{gore-sld-igpl}, \cite{wansing-displaying-modal-logic}. The generality of the display framework means that essentially the same meta-level proofs work for many different logics. A rigorous mechanical formalisation of such proofs is then widely applicable and worth pursuing. In this paper we discuss the implementation of \dRA, a display calculus for relation algebras, as a case study for exploring various methods for such a mechanical formalisation of display calculi in general. \comment{ Display calculi resemble the Gentzen sequent calculus \textbf{LK}, but with significant differences. For example, the rules for introducing the connective `$\lor$' (on the right) in \textbf{LK} and some display calculi are \label{|-v} $$\frac {\Gamma \vdash \Delta, P, Q} {\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor ) \qquad \textrm{ and } \qquad \frac {X \vdash P , Q} { X \vdash P \lor Q}(\mbox{DC-}\vdash \lor ) $$ Whereas, in \textbf{LK}, $\Gamma$ and $\Delta$ denote comma-separated lists of formulae, in a display calculus, $X$ denotes a \emph{structure}, which can involve several \emph{structural} connectives (one of which is `,'). A structure can be either a \emph{formula} (such as $P$ or $P \lor Q$) or the result of a structure operator acting on smaller structure(s) (such as $P , Q$). Display calculi extend the Gentzen calculus with extra structural connectives, such as `*' (meaning negation) and, for \dRA, operators with relational meanings. } Display calculi extend Gentzen's language of sequents with extra, complex, $n$-ary structural connectives, in addition to Gentzen's sole structural connective, the ``comma''. Whereas Gentzen assumed the comma to be associative, commutative and inherently poly-valent, display calculi make no such implicit assumptions. Properties such as these are explicitly stated as structural rules. For example, \dRA-sequents are built using a binary comma, a binary semicolon, and unary $*$ and $\bullet$ structural connectives. Thus, whereas Gentzen's sequents $\Gamma \vdash \Delta$ assume that $\Gamma$ and $\Delta$ are comma-separated lists of formulae, \dRA-sequents $X \vdash Y$ assume that $X$ and $Y$ are complex tree-like structures built from formulae together with comma, semicolon, $*$ and $\bullet$. The defining feature of display calculi is that in all logical introduction rules, the principal formula is always ``displayed'' as the whole of the right-hand or left-hand side. For example, the rule $(\mbox{\textbf{LK}-}\vdash \lor )$, shown below left, is typical of Gentzen's sequent calculi like \textbf{LK}, while the rule $(\mbox{\dRA-}\vdash \lor )$ shown on the right is typical of display calculi: $$\frac {\Gamma \vdash \Delta, P, Q} {\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor ) \qquad \qquad \frac {X \vdash P , Q} { X \vdash P \lor Q}(\mbox{\dRA-}\vdash \lor ) $$ Intuitively, to use this display calculus rule downwards on a sequent $X' \vdash Y'$, everything other than $(P,Q)$ %that ``belongs on the right of $\vdash$'' must be moved into the complex structure $X$ on the left of $\vdash$, thereby displaying the structure $(P,Q)$ as the whole of the right-hand side. There are rules which enable any given structure to be displayed. After the rule application we can ``undisplay'' the moved material back to its original position (reversing the display steps used), so that the sole purpose of this rule is to ``rewrite'' some $(P,Q)$ to $P \lor Q$ somewhere inside $Y'$. See \cite{gore-relalg} for a full account. Isabelle is an automated proof assistant \cite{isabelle-ref}. Its meta-logic is an intuitionistic typed higher-order logic, % and typed $\lambda$-calculus, sufficient to support the built-in inference steps of higher-order unification and term rewriting. Isabelle accepts inference rules of the form ``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$'' where the $\alpha_i$ and $\beta$ are expressions of the Isabelle meta-logic, or are expressions using a new syntax, defined by the user, for some ``object logic''. % $\mathcal F$. An Isabelle user can encode a particular calculus $\mathcal C _L$ for some logic $L$ as an ``object logic'' by using these rule templates to encode the set of inference rules of $\mathcal C _L$. %This is supplemented with the user's choice of %object logic in which to perform proofs. For example, if $\mathcal C _L$ is a natural deduction calculus, then the $\alpha_i$ and $\beta$ will be formulae of $L$, whereas if $\mathcal C _L$ is a sequent calculus, then the $\alpha_i$ and $\beta$ will be sequents of $\mathcal C _L$. Such an encoding is called an ``object logic'', even though it is a (typically natural deduction or sequent) \emph{calculus} for some particular logic $L$. In practice most users would build on one of the comprehensive ``object logics'' already supplied \cite{isabelle-object}. Twelf \cite{pfenning-schurmann-twelf} is an implementation of the Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework}, which is based on a typed $\lambda$-calculus with dependent types. Logics are represented using a \emph{judgements as types} principle, where each judgement of the form $\Gamma, x : Q \vdash y : P$ is identified with the types of its proofs. Twelf also accepts inference rules of the form ``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''. But now, the rule is expressed as the declaration of a $\lambda$-calculus term of type $\alpha_1 \to \alpha_2 \to \ldots \to \alpha_n \to \beta$. Once again, if the calculus we are trying to capture is a natural deduction calculus, then the $\alpha_i$ and $\beta$ will be formulae (types), but if the calculus is a sequent calculus, then the $\alpha_i$ and $\beta$ will be sequents (types). In an earlier paper \cite{dawson-gore-dra-jelia98}, we described the Isabelle implementation of \dRA, a display calculus for relation algebra \cite{gore-relalg}, as an object logic of Isabelle. In that paper we described how we had used the implementation to prove results comparing alternative formalisations of relation algebra from a proof-theoretic perspective. However we had not proved those results themselves \emph{in} Isabelle, in the sense we now explain. Suppose logic $L$ is a set of formulae which we regard as valid with respect to some semantics, and $\mathcal P$ and $\mathcal Q$ are two calculi for $L$ (each consisting of axioms and inference rules). Suppose also that we have mechanical implementations of $\mathcal P$ and $\mathcal Q$. Then one can use the implementation of $\mathcal P$ to derive in $\mathcal P$ every axiom and rule of $\mathcal Q$. One could then go outside the mechanical system and argue (by induction on the size, or structure, of a $\mathcal Q$-derivation) that therefore every $\mathcal Q$-derivable object (typically a formula or sequent) is also $\mathcal P$-derivable. In \cite{dawson-gore-dra-jelia98} we used the Isabelle \dRA\ implementation to show the soundness of certain other calculi for relation algebra. These results were proved in the manner described in the previous paragraph. An alternative and, when one's aim is the mechanical proof of proof-theoretic results, better approach would enable the inductive argument above to be carried out in the mechanical theorem-prover. This would require a different style of implementation of the calculi $\mathcal P$ and $\mathcal Q$ in the prover, so as to enable reasoning about the shape and form of $\mathcal P$-derivations and $\mathcal Q$-derivations. Typically this would require modelling, in the theorem prover, the ``tree'' of steps used in a derivation and the fact that each step is an instance of a rule of the calculus $\mathcal P$ or $\mathcal Q$; this in turn requires modelling the form of the statement of an inference rule of $\mathcal P$ or $\mathcal Q$, and a method of obtaining particular substitutional instances of such rules of inference. The terms ``shallow embedding'' and ``deep embedding'' are often used to distinguish these styles of implementation \cite{boulton-et-al-hdl}. Thus our work in \cite{dawson-gore-dra-jelia98} (see Section \ref{pure}) is an example of a shallow embedding, while the work reported in Section \ref{hol} is a deep embedding. Mikhajlova and von Wright \cite{mikhajlova-vonwright-isomorphism} used a deep embedding in their comparison of classical first-order logic proof systems. %and substitution of a term for a variable in it. This is the only other example of a deep embedding of a logical calculus of which we know. Other metamathematical results have also been mechanised -- see, eg, \cite{shankar}. % Providing both shallow and deep embeddings leads to the possibility of % linking the two implementations to give an efficient theorem prover % for \dRA, in the shallow embedding, but making use of proof-theoretic % results proved in the deep embedding. % We would then have a theorem prover based directly on machine-checked proof % theory. % The only other example % of a deep embedding of a logical calculus of which we know is found in % Mikhajlova and von Wright \cite{mikhajlova-vonwright-isomorphism}, % in which they compare classical first-order logic calculi. % % We contrast our approach with theirs in Section \ref{fwrw}. In this paper we compare methods of embedding \dRA\ in various logical frameworks. We explored the possibility of implementing a ``deep embedding'' in Twelf, Isabelle/CTT and Isabelle/HOL. In the subsequent sections we describe the original Isabelle/Pure implementation and this further work. \section{The Isabelle/Pure implementation} \label{pure} Isabelle is an interactive computer-based proof system, described in \cite{isabelle-ref}. Its capabilities include higher-order unification and term rewriting. It is written in Standard ML \cite{ML-definition}; the user can interact with it by entering further ML commands, and can program complex proof sequences in ML. As stated previously, the basic Isabelle constructs available to a user include inference rule templates of the form ``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''. These can be used ``forwards'', to obtain $\beta$ from the $\alpha_i$, or ``backwards'', to reduce a given goal $\beta$ to subgoals $\alpha_1, \alpha_2, \ldots, \alpha_n$. Isabelle provides a number of basic operations for backwards proof and proof-search (\emph{tactics}\index{tactic|textbf}), as well as \emph{tacticals}\index{tactical|textbf} for combining these. %Isabelle automatically keeps track of the subgoals generated by this backward %search procedure and the user can choose to work on any subgoal. %The user can also write complex proof tactics in ML; %many complex tactics and tacticals are supplied with %Isabelle or its standard object logics. Isabelle also supports forward proof. The inference rules collectively form a simple meta-logic: an intuitionistic typed higher-order logic. %typed $\lambda$-calculus. There are three logical operators: \texttt{==>} (implication, or deducibility), \texttt{==} (equality, or substitutability), and \texttt{!!} (universal quantification). For example, \mbox{\texttt{[| A1; A2 |]~==>~B}}, % which is an abbreviation for % \texttt{A1 ==> (A2 ==> B)}, is the Isabelle representation for ``from $\alpha_1, \alpha_2, \mbox{ infer } \beta$''. These operators satisfy certain properties arising from their intended meanings. For example, since %the Isabelle proposition \mbox{\texttt{[| A1; A2 |]~==>~B}} means that $\beta$ can be deduced from $\alpha_1$ and $\alpha_2$, % and can be proved by deducing $\beta$ % from $\alpha_1$ and $\alpha_2$, % we have that % \mbox{\texttt{[|~(A~==>~B);~A~|] ==> B},} % and that it is then possible to deduce $\beta$ from $\alpha_2$ and $\alpha_1$, i.e., \mbox{\texttt{[| A2; A1 |] ==> B}}. % Indeed, using Isabelle, we can prove a new rule that states % ``if (from $\alpha_1, \alpha_2, \mbox{ infer } \beta$) is a rule, % then (from $\alpha_2, \alpha_1, \mbox{ infer } \beta$) is a rule'', % as shown below: % \begin{center} % \texttt{[| [| A1; A2 |] ==> B |] ==> ([| A2; A1 |] ==> B)}. % \end{center} % %That is, \texttt{==>} can be seen as the analogue of the horizontal bar %used to state rules in a natural deduction system. % in which the order of premises is not significant. Likewise, since \texttt{A == B} means that \texttt{A} can be replaced by \texttt{B}, or vice versa, \texttt{==} is reflexive, symmetric and transitive. This meta-logic is known as Isabelle's Pure theory. In most cases the user would augment this by defining additional constants to capture the syntax of the object logic. For example, to capture set theory, we would add a constant \texttt{mem} (say) to stand for the $\in$ symbol, while sequents would require constants `\texttt{|-}' and `\texttt{,}'. % an object logic containing operators and inference rules; % these would usually include all the usual logical operators % and inference rules, % and often much more, such as operators and rules for set theory. Several such object logics are packaged with the Isabelle distribution \cite{isabelle-object}. Once these syntactic elements of the object logic are in place, we can build object-logic expressions into the $\alpha_i$ and $\beta$. For example, in \dRA, the $(\mbox{\dRA-}\vdash \lor )$ rule from Section 1 uses the meta-logical operator \texttt{==>} discussed above, and could be entered as \begin{center} \texttt{"\$X |- P, Q ==> \$X |- P v Q"}. \end{center} where the \texttt{\$} distinguishes \dRA-structures such as \texttt{X} from \dRA-formulae such as \texttt{P}. This rule is an instance of the form ``from $\alpha \mbox{ infer } \beta$''. In \cite{dawson-gore-dra-jelia98} \dRA\ was implemented in Isabelle directly on top of the Pure theory, so that the only inference rules available are those of \dRA. %(Thus you can't write $(P \vdash Q) \lor (R \vdash S)$, for example, %as you could if \dRA\ were built on top of Isabelle/HOL). As far as the Isabelle meta-logic is concerned, we can think of its atomic formulae as the formulae (for \dRA, the sequents) of the object-logic. In this case these are \dRA-sequents of the form $X \vdash Y$, built using object-logic ``connectives'' `$\vdash$', `,', `;', `*', `$\bullet$', `$\land$', `$\lor$', etc. These can be combined into more complex Isabelle propositions using the Isabelle meta-logic connectives \texttt{==>}, \texttt{==} and \texttt{!!}. % Thus each Isabelle proposition % is either a \dRA\ sequent $X \vdash Y$, or is % made up of sequents combined into inference rules % using the three Isabelle/Pure logical operators. It follows that expressions such as \texttt{\$X |- (P ==> Q)} or \texttt{A v (B ==> C)} are not possible. Note that the $\alpha_i$ and $\beta$ as discussed above would most commonly simply be \dRA-sequents, but could be ``complex'' Isabelle propositions, such as \texttt{\$X |- P ==> \$Y |- Q}. We may declare axioms and inference rules of the \dRA\ calculus to Isabelle. For example, the sequent $p \vdash p$ is an initial sequent (axiom) in \dRA; thus it is declared in Isabelle as a rule, \texttt{P |- P}, with no premises. % (For a rule with no premises, this notation is used rather than % \texttt{[| |] ==> P |- P}.) Similarly, each rule of \dRA\ is declared as an Isabelle rule, as in the example of the $(\vdash \lor)$ rule above. % This becomes an Isabelle theorem containing the metalogical % implication operator \texttt{==>}. % % These, and further derived sequents and rules, are called Isabelle % ``theorems''. %Isabelle theorems may be object logic formulae or may %involve Isabelle's metalogical operators. % Thus, in the Isabelle implementation of \dRA, an Isabelle theorem % may be either a simple sequent of \dRA, % or a sequent \emph{rule}. % Whereas a sequent derivable in % \dRA\ becomes an Isabelle theorem of the form \texttt{X |- Y}, % a sequent rule becomes an Isabelle theorem containing also % the operators \texttt{==>} (implication) or \texttt{==} (equality). That this is a shallow embedding is reflected in the fact that the horizontal bar of sequent rules becomes the Isabelle \texttt{==>} operator. In a deep embedding, as in Section \ref{hol}, the horizontal bar also becomes an object-level constant. \comment{ % For example, the (cut) rule (shown on \page{id}) appears as % {\par\noindent\centering % \texttt{"[| \$?X |- ?A; ?A |- \$?Y |] ==> \$?X |- \$?Y"} % \par\noindent} For example, the ($\vdash \lor $) rule (shown in \S\ref{|-v}) appears as $$\texttt{"\$?X |- ?A, ?B ==> \$?X |- ?A v ?B"}$$ in Isabelle. (The `\verb:?:' denotes a variable which can be instantiated, and the `\verb:$:' denotes a structural variable or constant.) The variant $A \vdash A$ of the (id) rule (see \S\ref{otm}) appears as \texttt{"?A |- ?A"}. The bi-directional \texttt{dcp} rule, shown in \fig{sdr}, appears as \texttt{"\$?X |- \$?Y == * \$?Y |- * \$?X"}. } In this shallow embedding, access to and manipulation of the shape of \dRA\ constructs (ie, sequents, structures, formulae) and derivations was provided only at the ML level. For example, in \cite{dawson-gore-dra-jelia98} we described having programmed a procedure to perform cut-elimination for \dRA. The input to this was a \dRA\ derivation (represented as a tree of sequent rule instances), and the output was a derivation not containing an instance of the cut rule. This required examining the shape of a derivation (represented as a tree of \dRA\ rule instances) and of the Isabelle terms representing sequents. While the shape of an Isabelle term is easily accessible (by ML code), % a derivation step is represented as a function. % a complex derivation is the composition of functions representing the % elementary derivation steps. % Therefore, to look at the shape of a derivation (for example, to ask % what rule was used in the final \dRA\ inference step) involved changing the we had to change the Isabelle code somewhat, so as to record the elementary \dRA\ rules used in a derivation, and to construct a derivation-tree which could be manipulated. % while a derivation was being performed. The aim of the work described in this paper is to perform the cut-elimination proof entirely within a theorem prover (rather than writing a cut-elimination program in ML). We therefore needed to model derivation trees, inference rules, substitution in them, and so on, % set of elementary inference rules of the calculus within the language of the theorem prover, as discussed in \S\ref{intro}. % so as to be able to say (for example) % that every rule in a given derivation tree % is an instance of one of the inference rules in that calculus. \comment{ In \cite{dawson-gore-dra-jelia98} we also described using the Isabelle \dRA\ implementation to show the soundness of certain other calculi for relation algebra. In these cases, we in fact showed that all the axioms and rules of the other calculi were derivable in \dRA. The argument that followed, namely that therefore an entire derivation in one of those other calculi could have been performed in \dRA, was outside the scope of the mechanical theorem prover. Again, doing this within the theorem prover would have required modelling the shape of sequents or formulae of the calculus in question, of derivations, and of the rules used in them. This was done by Mikhajlova and von Wright \cite{mikhajlova-vonwright-isomorphism} in their comparison of classical first-order logic proof systems. } % But note that their work assumes that the second and third % clauses of the definitions given at % \cite[p.~302]{mikhajlova-vonwright-isomorphism} are sound, % and we suspect one is not. % We are currently trying to show whether their definitions % are derivable using their previous definitions. \section{Dependent Type Theory implementations} \subsection{Introduction} In a dependent type theory, a type may be parametrised not only over a type variable, but also over a term variable. This, coupled with the \emph{judgements as types} principle (where a judgement is identified with the types of its proofs) enables us to express the derivation of a display calculus derived rule. A simpler example of a Curry-Howard isomorphism is between the simply-typed $\lambda$-calculus and a natural deduction calculus \textsf{NDInt} for intuitionistic propositional logic. Let $A$ and $B$ be formulae, and $\pi$ be a derivation of $A$ in \textsf{NDInt}. Suppose also that $A \to B$ is derivable in \textsf{NDInt}, and consider an \textsf{NDInt}-derivation of $A \to B$ %in the Natural Deduction style, where one assumes $A$ and derives $B$. That is, it is a derivation of $B$ in which $A$ is regarded as true; at the points where $A$ is used, it would contain some notation $\xi$ meaning ``true by assumption''. Let $\rho(\xi)$ be this derivation of $B$. %where $x$ is a place-holder for some %notation meaning ``true by assumption'', %as will appear in the derivation of $B$ wherever $A$ is used. So if we substitute $\pi$ (the derivation of $A$) for $\xi$ in $\rho(\xi)$, we get a derivation $\rho(\pi)$ of $B$ which does not rely on $A$ as an assumption. Then, using $\pi : A$ to mean ``$\pi$ is a derivation of $A$'', we can write the rule \begin{center} \slrule { \pi : A \qquad \rho(\xi) : A \to B } { \rho(\pi) : B } \end{center} Erasing the annotations $\pi$, $\rho$ and `:' gives the well-known $(\to E)$ natural deduction rule for intuitionistic logic; the rule as it stands also shows how to derive $B$. As indicated above, we can equally think of $\rho(.)$ as a derivation of $A \to B$ or as a function which takes, as argument, a derivation of $A$ such as $\pi$, and returns a derivation of $B$. If we also think of $A$ as the type ``derivations of proposition $A$'' (and similarly for $B$) we get the functional type-theory interpretation, under which $A \to B$ means the type of functions which take an argument of type $A$ and return a result of type $B$. (Conveniently, the same symbol `$\to$' is conventionally used for both purposes.) Dependent types extend what can be done in the simply-typed $\lambda$-calculus in two distinct ways. Firstly, consider a type $I$ of individuals, and a parametrised type $A(i)$; that is, for each individual $i \in I$, there is a type $A(i)$. Then the dependent type $A$ corresponds to a predicate $A$ on $I$, and the type $A(i)$ to the proposition $A(i)$. \comment{ Consider a function $\rho$ whose domain is $I$, such that for each $i \in I$, $\rho(i) \in A(i)$. The type of such a function is written $\prod i : I . A(i)$ (denoting how the \emph{type} of $\rho(i)$ \emph{depends} on the \emph{value} of $i$). Now let $A$ be a predicate, and therefore each $A(i)$ be a proposition (taking the value true or false), and let each $\rho(i)$ be a derivation of $A(i)$. That is, $\rho$ is a function which, for each individual $i$, gives a derivation of $A(i)$; we can think of such a $\rho$ as a derivation of $\forall i A(i)$. At the same time, if we think of each type $A(i)$ as the type ``derivations of proposition $A(i)$'', then the functions $\rho$ of type $\prod i : I . A(i)$ are the derivations of $\forall i A(i)$. } Secondly, we install an object logic at the level of terms, so that the expressions (formulae or sequents) of the object logic become terms of the dependently-typed $\lambda$-calculus. That is, we can install a syntax for terms using the syntax of the chosen object logic, and declare a type constructor $P(.)$, so that for each term $t$, $P(t)$ will mean ``derivation of expression $t$''. This was our approach for modelling \dRA. % (though instead of $P(t)$, we used $X \vdash Y$, % the two arguments $X$ and $Y$ being % the left and right-hand sides of a sequent). Regarding an expression (formula or sequent) $t$ as derivable when we have a term of type $P(t)$ has certain consequences. For example, since from functions of type $X \to Z$, $U \to V \to W$ and $S \to S \to T$ we can construct functions of type $X \to Y \to Z$, $V \to U \to W$ and $S \to T$, we unavoidably have weakening, exchange and contraction. Note, however, that in our formulation of \dRA, these are in the meta-logic level, not in the object logic. Two theories based on dependent types are the Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework} and Constructive Type Theory (CTT) \cite{martin-lof-CTT}. \subsection{The Twelf implementation} Twelf \cite{pfenning-schurmann-twelf} is an implementation of the Edinburgh Logical Framework (LF) \cite{harper-honsell-plotkin-framework}. This is based on a typed $\lambda$-calculus with dependent types. Twelf is written in Standard ML, and the user can interact with the system using its ``ML Interface'', but only a limited range of functions is available. Figure \ref{fig:twelf-source} is an extract of our Twelf source file. \begin{figure}[htbp] \normalsize \begin{center} \begin{tabular}{c@{\quad}l} 1 & \texttt{struct : type. } \\[-1.5ex] 2 & \texttt{|- : struct -> struct -> type.} \\[-1.5ex]% \%infix none 10 |-.} \\ 3 & \texttt{* : struct -> struct.} \\%\%prefix 200 *.} \\ 4 & \texttt{\% Display postulates } \\[-1.5ex] 5 & \texttt{sA : (* X |- Y) -> (* Y |- X).} \\[-1.5ex] 6 & \texttt{sS : (X |- * Y) -> (Y |- * X).} \\ 7 & \texttt{\% Derived structural rules} \\[-1.5ex] 8 & \texttt{ssASl = [D] sA (sS D).} % \% (X |- * * Y) -> (* * X |- Y)} \end{tabular} \end{center} \caption{Sample Twelf source code} \label{fig:twelf-source} \end{figure} Line~1 declares \texttt{struct} as a new type to represent the \dRA\ structures. Line~2 declares \texttt{|-} as a binary type constructor, taking two \emph{term} arguments of type \texttt{struct} and returning a \emph{type}. Following the description above, we should declare \texttt{sequent} as a new type to represent \dRA\ sequents, and \texttt{P} as a function taking a \emph{term} argument of type \texttt{sequent} and returning a \emph{type}, thus: \begin{quote} \texttt{sequent : type. } \\ \texttt{|- : struct -> struct -> sequent. } \\% \%infix none 10 |-. \texttt{P : sequent -> type.} \end{quote} The actual code in Figure \ref{fig:twelf-source} abbreviates this by removing the type constructor \texttt{P} and (in effect) changing \texttt{|-} from a term constructor to a type constructor. Thus, for structures \texttt{X} and \texttt{Y}, the construct \texttt{X |- Y} represents derivations of the sequent $X \vdash Y$. (We did this only to simplify the printed output). Line~3 declares \texttt{*} as a unary structure operator. Lines 4 and 7 are comments. In lines 5 and 6 the terms \texttt{sA} and \texttt{sS} are declared with the types %showing that they denote that represent derivations of the \dRA\ rules (see \cite{gore-relalg}) shown below: \begin{center} \slrule { *X \vdash Y } { *Y \vdash X } (\ttdef{sA}) \qquad \hspace{20mm} \slrule { X \vdash *Y } { Y \vdash *X } (\ttdef{sS}) \qquad \end{center} We can think of these declarations as assertions that there are derivations (which we name \texttt{sA} and \texttt{sS}) of these rules, or as defining these as ``primitive'' rules (one-step derivations). Now, treating \texttt{sA} and \texttt{sS} (which stand for ``star in the antecedent'' and ``star in the succedent'') as functions each taking a derivation of a sequent to a derivation of another sequent, they can be composed for some given sequent $U \vdash * * V$ as follows $$ \stackrel {\mbox{derivation of}}{U \vdash * * V} \quad \stackrel{\texttt{sS}} \longrightarrow \quad \stackrel {\mbox{derivation of}}{* V \vdash * U} \quad \stackrel{\texttt{sA}} \longrightarrow \quad \stackrel {\mbox{derivation of}}{* * U \vdash V} $$ The definition of \texttt{ssSAl} on line 8 does this; the notation means $\lambda D. \textit{sA} (\textit{sS} \ D)$. Twelf computes the type of \texttt{ssSAl}, giving $(S1 \vdash * * S2) \to (* * S1 \vdash S2)$. Note that $X, Y, S1$ and $S2$ are variables ($S1$ and $S2$ being names chosen by Twelf). In a manner akin to Prolog \cite{prolog-standard}, Twelf allows one to make a query such as \begin{center} \texttt{ \_ssASl : (X1 |- * * Y1) -> (* * X1 |- Y1).} \end{center} \noindent which searches for a term of the specified type (i.e., searches for a derivation of the stated rule) and instantiates \texttt{\_ssASl} with that term. In this example, because Twelf allows substituting for \texttt{X1} and \texttt{Y1} in the query as well as for the variables \texttt{X} and \texttt{Y} in the declarations of \texttt{sA} and \texttt{sS}, the search proceeds along an infinite branch in the wrong direction. On the other hand, the code \begin{verbatim} %theorem ssASl_th : exists {DerivedRule:{S1:struct} {S2:struct} (S1 |- * * S2) -> (* * S1 |- S2)} true. %prove 2 {} (ssASl_th DerivedRule). \end{verbatim} \noindent successfully uses Twelf's theorem prover to find the derivation, returning \begin{verbatim} /ssASl_th/: ssASl_th ([S1:struct] [S2:struct] [D:S1 |- * * S2] sA (sS D)). \end{verbatim} \noindent (Here the variables \texttt{S1} and \texttt{S2} need to be explicitly abstracted over -- in the earlier code they were free variables). Twelf's theorem prover is not extensively documented, and is stated to be under active development, with the proof search component expected to undergo major changes. The proof search strategy can be controlled by the user to only a limited extent, whereas we have found that considerable user control (using tactics differing from proof to proof) is generally necessary in our work. We found that certain aspects of Isabelle which we very much appreciated are absent from Twelf. Isabelle offers a substantial number of user ``commands'', in the form of documented ML functions, which enable the user to programme proof procedures, or to examine the shape of a term or type expression. For example, one might write a tactic which explicitly examines the current proof state and then decides which of several tactics to apply. There are many expressive ``glue'' functions for combining tactics in Isabelle. Inadequacies in the documentation, or in the selection of functions documented, can often be circumvented by looking at the source code, which can also be a great help to the user in programming his/her own tactics. At this stage, Twelf does not appear to offer comparable capabilities to the user. Thus, although the theorem prover did successfully find the derivation above, we felt uncertain that we could use it to find all required derivations, primarily because of the lack of user control over a proof. \subsection{The Cut-Elimination Theorem in Twelf} At this point we should refer to the proof of a cut-elimination theorem, using Twelf, described in \cite{pfenning-structural-cut-elimination}. This uses a rather ingenious representation of sequents; a cut-free proof of a traditional Gentzen sequent $A \vdash B$ is represented as the type \texttt{neg A -> pos B -> @}, and a cut-free proof of it as \texttt{neg A -> pos B -> \#}, as explained in \cite{pfenning-structural-cut-elimination}. The two rules shown below left are both represented as the type shown on the right: \begin{center} \slrule {\Gamma, A \vdash \Delta} {\Gamma, A \& B \vdash \Delta} \quad \slrule { A \vdash } { A \& B \vdash } \quad \texttt{(neg A -> \#) -> (neg (A and B) -> \#)} \end{center} In fact, the second rule shown would be directly represented by the type shown, but the first rule shown could be directly represented by \begin{quote} \texttt{(neg $\Gamma$ -> pos $\Delta$ -> neg A -> \#) -> \\ \mbox{} \quad (neg $\Gamma$ -> pos $\Delta$ -> neg (A and B) -> \#)} \end{quote} However the existence of a term (function) of the type shown first trivially implies the existence of a term (function) of the type shown second. Further constructed types represent stages of the transformation of a proof into a cut-free proof, and a termination checker checks that the function performing the entire transformation from a proof to a cut-free proof terminates. However, this termination checker only checks that the function would not run forever. It does not check that it terminates with a cut-free derivation -- it does not complain if the code is run with some cases deleted. This work on the cut-elimination theorem is based on an ingenious way of representing the problem in a way that fits into Twelf; even so, getting a proof of the cut-elimination theorem from it relies on the heuristically-based termination checker and upon a manual check that all possible cases for the rules used just above the ``cut'' have been covered. On the other hand, the Twelf type-checker proves that each individual step is correct, in that the changed derivation in fact does derive the sequent which it purports to derive. Thus this proof of cut-elimination lies between our previous work (where we just programmed a cut-elimination function in ML) and a fully formal proof. \subsection{The Isabelle/CTT implementation} We then turned to the \texttt{CTT} theory of Isabelle, since it is based on a logic which is very similar to that of Twelf, in that it includes dependent types. % We implemented \dRA\ similarly to its implementation in Twelf, so that we had, for example, (omitting premises of the form \texttt{?X : str}) %, which were fairly ubiquitous) \texttt{ \begin{quote} "sA : * ?X |- ?Y --> * ?Y |- ?X" : thm \\ "sA oo sS : ?X |- * * ?Y --> * * ?X |- ?Y" : thm \end{quote} } \comment{ \begin{center} \begin{tabular}{l} "sA : * ?X |- ?Y --> * ?Y |- ?X" : thm \\ "sA oo sS : ?X |- * * ?Y --> * * ?X |- ?Y" : thm \end{tabular} \end{center} } \noindent where \texttt{oo} denotes function composition. Tactics were written to determine the type of a term (ie, to determine the derived rule obtained by a given combination of rules), by solving a goal such as \texttt{sA oo sS : ?t} (which contains the type variable \texttt{?t}). We explored tactics to search for a term of a given type (ie, a proof of a given term), by solving a goal such as the one below, which contains the term variable \texttt{?P}. \begin{center} \texttt{"?P : ( X |- * * Y) --> ( * * X |- Y)"}. \end{center} The \texttt{CTT} theory of Isabelle is not as extensively developed as some other theories are; we found it necessary to prove some general but elementary theorems. %\subsection{Dependent type theory -- conclusions} \subsection{Conclusions} We experimented with Twelf because it had appeared that we would get our hands on the proofs ``for free'', in that in the course of deriving a sequent or sequent rule, we produce a term which embodies the derivation performed. Given our intention to do a fully mechanised proof of the cut-elimination theorem (in which we manipulate derivations extensively) it had seemed that this feature of Twelf would be useful. Our work with Isabelle/CTT seemed to indicate that the same things could be done in it as in Twelf (with some effort to produce appropriate derived rules and tactics). However we realised that although we could produce a term which represented the derivation and showed the elementary steps from which it is composed, we could not analyse derivations, \emph{in the logic of the theorem prover}, in the required ways: for example, to ask which rule was used in the final step of the derivation. In the light of this, there seemed to be no benefit in pursuing an implementation using dependent type theory. We have referred to a proof in Twelf of the cut-elimination theorem, noting that it was based on an ingenious way of representing the problem in a way that fits into Twelf, and that it was not a fully formal proof. Since we are aiming for a formal proof, using techniques which would apply equally for other proof-theoretic results, we felt that this cut-elimination proof does not indicate that dependent type theory would be powerful enough for our needs. \section{The Isabelle/HOL implementation} \label{hol} \texttt{HOL} is an Isabelle theory based on the higher-order logic of Church \cite{church-types} and the HOL system of Gordon \cite{HOL-introduction}. Thus it includes quantification and abstraction over higher-order functions and predicates. The \texttt{HOL} theory uses Isabelle's own type system and function application and abstraction (that is, object-level types and functions are identified with meta-level types and functions). Isabelle/HOL contains constructs found in functional programming languages (such as \texttt{datatype} and \texttt{let}) which greatly facilitates re-implementing a program in Isabelle/HOL, and then reasoning about it. However limitations (not found in, say, Standard ML itself) prevent defining types which are empty or which are not sets, or functions which may not terminate. Isabelle/HOL turned out to be entirely suitable for the deep embedding of \dRA. The most significant factor leading us to this conclusion is the facility for \texttt{datatype} type declarations and associated primitive recursive function definitions, which was enormously helpful. For example, we model \dRA\ structure expressions (see \cite{gore-relalg}) as follows \begin{verbatim} datatype structr = Comma structr structr | SemiC structr structr | Star structr | Blob structr | I | E | Structform formula | SV string \end{verbatim} The first six lines correspond to the structure operators of \dRA\ and the next line is for ``casting'' a formula of \dRA\ as a structure of \dRA. The last line had no analogue in the shallow embedding, where we just used an Isabelle variable such as \texttt{?S} to refer to any \dRA-structure. In the deep embedding, \texttt{SV ``X``} refers to the structure variable named \texttt{X} appearing in (say) the statement of a rule. Thus we can now write \texttt{SV ?V}, which Isabelle will match with a structure expression consisting of a single structure variable, or \texttt{?S} to match any structure. We also defined functions (in Isabelle/HOL) which (for example) find all the variables in a structure expression, or substitute a given structure for such a variable. We also wrote such functions for the work described in \S\ref{pure}, but in Standard ML, not in Isabelle. \comment{ On the other hand, when writing Isabelle tactics which involve analysing the shape of a rule, we could write (for example) \texttt{((SV ?V), ?S)} to match any structure expression consisting of two substructures joined by the comma operator (infix `\texttt{,}' is alternative notation for prefix \texttt{Comma}), of which the first must be a structure variable. This matching and any related substitution is performed by Isabelle. } For describing the structure of a derivation we have \begin{verbatim} datatype pftree = Pr sequent rule (pftree list) | Unf sequent \end{verbatim} where \texttt{Pr seq rule pts} is a derivation of the sequent \texttt{seq}, the last step of the derivation uses the \dRA\ rule \texttt{rule}, and the premises of that last step are the conclusions of the derivations in the list \texttt{pts}. \ \ \texttt{Unf} (``unfinished'') means that a leaf is a sequent which is not an axiom, so is an assumption (or a ``premise'') of the derivation tree as a whole. \comment{ We define functions which check that such a structure is a valid derivation (for example, that the premises of an instantiated rule really are the conclusions of the trees above, and that each step uses a legitimate rule). For example, to list the ``premises'' of the whole derivation tree: \begin{verbatim} primrec "premsPT (Unf seq) = [seq]" "premsPT (Pr seq rule pts) = premsPTs pts" "premsPTs [] = []" "premsPTs (pt # pts) = (premsPT pt @ premsPTs pts)" \end{verbatim} Each datatype declaration generates a number of theorems which are made available for proofs, and of which some are installed in rule sets used by the more automated proof tactics. These theorems include ones expressing that a \texttt{datatype} type is a disjoint union and that the constructors are 1-1 functions, and one expressing a structural induction principle. } We give examples of results which show how we can reason about provability in this embedding. Here \texttt{IsProvableR rules prems concl} means that sequent \texttt{concl} can be derived from sequents \texttt{prems} using rules \texttt{rules}, and \texttt{IsProvable rules rule} means that the conclusion of the statement of \texttt{rule} may be derived from its premises using \texttt{rules}. \begin{verbatim} val IsProvableR_trans = "[| IsProvableR rules prems' concl ; ALL p:prems'. IsProvableR rules prems p |] ==> IsProvableR rules prems concl" val IsProvableR_deriv = "[| ALL rule:rules'. IsProvable rules rule ; IsProvableR rules' prems concl |] ==> IsProvableR rules prems concl" \end{verbatim} While we think that the corresponding results, for particular instances of the sequents and derivations involved, could be proved more easily in Twelf than in Isabelle, we cannot see how to express the general results in Twelf or Isabelle/CTT, without, in effect, doing a deep embedding in those systems, as mentioned in the next section. \section{Further work and Related Work} \label{fwrw} A proof of the cut-elimination theorem for \dRA\ has been completed, and will be reported in another paper. Using the deep embedding into Isabelle/HOL, we were able to specify and reason about derivability and derivation trees. \comment{ for example, we expressed the requirement that each step of a derivation uses a substitution instance of a \dRA\ rule found in a given set. Reasoning about derivability and derivation trees is rather intricate. We note that in other work of this nature \cite[p.~302]{mikhajlova-vonwright-isomorphism} the authors chose to state, rather than prove, principles concerning the transitivity of provability, and provability from derived rules. (See the second and third clauses of the definitions given at \cite[p.~302]{mikhajlova-vonwright-isomorphism}). We have been able to prove corresponding rules from our definition of a proof tree. These are the theorems \texttt{IsProvableR\_trans} and \texttt{IsProvableR\_deriv} given near the end of Section \ref{hol}. Proving rather than stating such rules is preferable as it avoids the possibility of stating an unsound rule. Interestingly, we doubt the suitability of the requirement for a derived rule used in \cite{mikhajlova-vonwright-isomorphism}, in the third clause of their definition of \texttt{IsProvable}. Looking at the code given in the paper, the phrase \begin{verbatim} (?inf. CorrectRuleInst {r} inf /\ IsProvable rSet (InfHyps inf) (InfConcl inf)) \end{verbatim} suggests requiring that only one (not all) of the instances of the derived rule \texttt{r} be provable, which would allow using \texttt{P ==> Q} as a derived rule because \texttt{False ==> True} is provable. } Clearly the Isabelle/HOL logic is well-equipped for writing specifications which describe the process of performing proofs by substituting for variables in the rules of a given logical calculus. We attribute this to the richness of the logic, containing not only sum and product types, but recursive datatypes (as in the programming languages ML and Haskell), and to the fact that Isabelle/HOL provides the theorems which characterise each such type. %It was easy to specify the behaviour of a program %written in functional programming style, and for reasoning about it. It was thus a suitable choice for this project. As one of the referees has pointed out, our final embedding of \dRA\ into Isabelle/HOL is very deep, making use of recursive datatypes and other features of Isabelle/HOL. The need for such a deep embedding was discovered in the process of trying out the various shallow embeddings and finding them unsuitable for our proof-theoretical needs. An interesting question is whether an equally deep embedding of \dRA\ would be feasible in Isabelle/Pure, Isabelle/CTT and Twelf. Our personal view is that this would be possible, but that such an embedding would be extremely complicated and difficult because we would have to virtually reimplement essential features such as recursive datatypes which are not available in Isabelle/Pure, Isabelle/CTT or Twelf. \comment{ Another concept requiring further exploration is using the types of Twelf or Isabelle/CTT to express more than just the sequent being proved. For example, one might let $t : P(X \vdash Y, \rho, n)$ denote that $t$ is a derivation of $X \vdash Y$, of length at most $n$, where the last rule used is $\rho$. Clearly, however, to get all the expressiveness we need in this way would require far more complex type expressions than in this example: doing this may be tantamount to doing a deep embedding without the helpful features of Isabelle/HOL, such as \texttt{datatype}s. } We aimed to produce a ``deep'' embedding of display calculi, sufficient (for example) to enable a mechanised proof of the cut-elimination theorem. While we have done this (in a sense), our work has elucidated some further points. Belnap's cut-elimination theorem for display calculi is generic. It applies to all display calculi whose rules satisfy certain conditions. We have modelled a particular display calculus, \dRA\ (for relation algebra). Accordingly, we have proved the cut-elimination theorem for \dRA. While we can identify the properties of the \dRA\ rules used in the proof, and match these with Belnap's conditions, we have not proved the theorem as stated by Belnap (which applies to \emph{any} display calculus). To model an arbitrary display calculus in Isabelle/HOL would be a further (and harder) activity. \comment{ Secondly, Belnap's conditions on the rules of the display calculus are listed by Kracht \cite{kracht-power}, who states ``These conditions actually need some exegesis''. Our work will produce a precise, formal, statement of those properties of the rules which we actually use in the proof of the theorem. } \section{Conclusion} We have reviewed earlier work which described a shallow embedding of the \dRA\ calculus into the Isabelle/Pure logic, and noted its drawbacks for proving proof-theoretic results in Isabelle itself. Attracted by the notion that the tools based on dependent type theory would give expressiveness about proofs ``for free'', we then looked at the Twelf tool. While the Twelf tool is still under active development, we noted how a similar logic is available in Isabelle/CTT, which offers the advantages of Isabelle, such as access to a wide range of documented ML functions for programming proof tactics. However we also found that, while Twelf and Isabelle/CTT facilitate identifying the derivation of a sequent or derived rule, they do not facilitate reasoning about the shape of that derivation, or of the sequents found in it. Thus we turned to Isabelle/HOL, which appears to offer the best facility for deeply embedding a calculus such as \dRA, and reasoning about derivability, derivation trees and the associated proof-theoretic concepts we needed. Needless to say, this was the advice we received from Larry Paulson from the start. \begin{ack} We are grateful to Paul Jackson, Randy Pollack and Mark Staples for many useful discussions on the notions of ``shallow'' and ``deep'' embeddings, to Frank Pfenning and Larry Paulson for answering our questions about Twelf and Isabelle, and to Jim Grundy for helpful comments. \end{ack} \comment{ } %endcomment %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Here begins the end matter \begin{thebibliography}{10} \bibitem{belnap-display} N~D {Belnap}. \newblock Display logic. \newblock {\em Journal of Philosophical Logic}, 11:375--417, 1982. \bibitem{boulton-et-al-hdl} R~J Boulton, A~D Gordon, M~J~C Gordon, J~R Harrison, J~Herbert, and J~van Tassel. \newblock Experience with embedding hardware description languages in {HOL}. \newblock {\em Proc.\ Intl.\ Conf.\ on Theorem Provers in Circuit Design: Theory, Practice and Experience}, IFIP Trans.\ \newblock volume A-10:129--156. North-Holland/Elsevier, 1992. \bibitem{church-types} A~Church. \newblock A formulation of the simple theory of types. \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940. \bibitem{dawson-gore-dra-jelia98} J~Dawson and R~Gor{\'{e}}. \newblock A mechanised proof system for relation algebra using display logic. \newblock In {\em JELIA98: Logic in Artificial Intelligence}, \newblock LNAI 1489:264--278. Springer, 1998. \bibitem{prolog-standard} P~Deransart, A~Ed-Dbali, and L~Cervoni. \newblock {\em Prolog: The Standard}. \newblock Springer-Verlag, 1996. \bibitem{elmasri-navathe-database} R~A Elmasri and S~B Navathe. \newblock {\em Fundamentals of Database Systems}. \newblock Benjamin/Cummings, Redwood City, 2 edition, 1994. \bibitem{gallier-logic} J.~H. Gallier. \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem Proving}. \newblock John Wiley and Sons, 1987. \bibitem{HOL-introduction} M~J~C Gordon and T~F Melham. \newblock {\em Introduction to HOL: a Theorem Proving Environment for Higher Order Logic}. \newblock Cambridge University Press, 1993. \bibitem{gore-relalg} R~Gor{\'{e}}. \newblock Cut-free display calculi for relation algebras. \newblock In {\em CSL96: Computer Science Logic}, LNCS 1258:198--210, \newblock Springer, 1997. \bibitem{gore-sld-igpl} R~Gor{\'{e}}. \newblock Substructural logics on display. \newblock {\em Logic Journal of the Interest Group in Pure and Applied Logic}, 6(3):451--504, 1998. \bibitem{harper-honsell-plotkin-framework} R~Harper, F~Honsell, and G~Plotkin. \newblock A framework for defining logics. \newblock {\em Journal of the ACM}, 40:143--184, 1993. \bibitem{maddux-introductory} R~D Maddux. \newblock Introductory course on relation algebras, finite-dimensional cylindric algebras, and their interconnections. \newblock In {\em Algebraic Logic}, {\em Colloquia Mathematica Societatis Janos Bolyai}, Volume~54:361--392. North-Holland, 1991. \bibitem{martin-lof-CTT} P~Martin-L\"{o}f. \newblock {\em Intuitionistic Type Theory}. \newblock Bibliopolis, 1984. \bibitem{mikhajlova-vonwright-isomorphism} A~Mikhajlova and J~von Wright. \newblock Proving isomorphism of first-order proof systems in {HOL}. \newblock In {\em Theorem Proving in Higher-Order Logics}, LNCS 1479:295--314. \newblock Springer, 1998. \bibitem{mili-relational} A~Mili. \newblock A relational approach to the design of deterministic programs. \newblock {\em Acta Informatica}, 20:315--328, 1983. \bibitem{ML-definition} R~Milner, M~Tofte, R~Harper, and D~MacQueen. \newblock {\em The Definition of Standard ML (Revised)}. \newblock The MIT Press, 1997. \bibitem{isabelle-ref} L~C Paulson. \newblock {\em The Isabelle Reference Manual}. \newblock Computer Laboratory, University of Cambridge, 1999. \bibitem{isabelle-object} L~C Paulson. \newblock {\em Isabelle's Logics}. \newblock Computer Lab.\, Univ.\ of Cambridge, 1999. \bibitem{pfenning-structural-cut-elimination} F~Pfenning. \newblock Structural cut elimination. \newblock In {\em Proc.\ Tenth Annual Symposium on Logic in Comp.\ Sci.\ }, pages 156--166. IEEE Computer Society Press, 1995. \bibitem{pfenning-schurmann-twelf} F~Pfenning and C~Sch\"{u}rmann. \newblock System description: Twelf - a meta-logical framework for deductive systems. \newblock In CADE-16 {\em Proc.\ 16th Intl.\ Conf. on Automated Deduction }, \newblock LNAI 1632:202--206. Springer, 1999. \bibitem{shankar} Natarajan Shankar. \newblock {\em Metamathematics, Machines, and Goedel's Proof}. \newblock Cambridge University Press, 1994. \bibitem{wansing-displaying-modal-logic} Heinrich Wansing. \newblock {\em Displaying Modal Logic}, volume~3 of {\em Trends in Logic}. \newblock Kluwer Academic Publishers, Dordrecht, August 1998. \end{thebibliography} \end{document}