> Collecting proofs of the same theorem in various proof checking systems
> may be useful for preparing a thorough comparative survey of existing
> systems( I would be grateful for any references on such surveys already
> published).
The following manuscript may be interesting to you:
Sten Agerholm, Ilya Beylin, and Peter Dybjer
A Comparison of HOL and ALF:
Formalizations of a Categorical Coherence Theorem
\begin{abstract}
We compare the systems HOL, which implements an extension of Church's
classical simple type theory, and ALF, which implements an extension of
Martin-L\"of's intuitionistic type theory, with respect to the formalization
of a piece of elementary category theory: the proof of coherence for monoidal
categories. This proof was originally developed as an example of program
extraction from constructive proof. It shows how the proof of coherence for
monoidal categories can be extracted from a proof of normalization for
monoids and makes essential use of the identification of proofs and programs
which is fundamental to intuitionistic type theory. This aspect of the proof
is naturally highlighted in the ALF formalization. However, it was possible
to develop a quite parallel formalization in HOL without this focus. The
most interesting aspect of the development concerned the implementation of
diagram chasing. In particular, the HOL development was greatly facilitated
by an implementation of tool support for equational reasoning in Standard ML.
\end{abstract}
It is available on ftp://ftp.cs.chalmers.se/pub/users/ilya/FMC/hol_alf.ps.gz
and the correspondent ALF proof can be found in the same directory
or on the web http://www.cs.chalmers.se/~ilya/FMC.
Ilya Beylin <ilya@cs.chalmers.se>
Department of Computer Science,
Chalmers University of Technology, Phone: +46-31-772-1079
S-41296 Gothenburg, Sweden Fax: +46-31-165655