\documentclass[a4paper]{llncs}
%\usepackage[T1]{fontenc}
\usepackage{salt-light}
\usepackage{graphicx}

\usepackage{mathwiki}

\title{\thetitle}

\author{\theauthors}

\institute{\theinstitute}

\begin{document}

\maketitle

\begin{abstract}

\hspace{-.1pt}Mathematical documents, and their instrumentation by computers, have
rich structure at the layers of presentation, metadata and semantics,
as objects in a system for formal mathematical logic. Semantic Web
tools~\cite{openmath} support the first two of these, with little, if any,
contribution to the third, while Proof Assistants~\cite{wiedijk06-17provers}\weg{Computer Mathematics
\cite{barendregtwiedijk,barendregtcohen}}\weg{, or Interactive Theorem
Proving,} instrument\weg{s}%
\weg{formal logic, typically with bespoke approaches to
the first and second layers, in its so-called Proof Assistants.} 
the third layer, typically with bespoke approaches to
the first two. 
%%%
Our position is that a web of mathematical documents, definitions
and proofs should be given a fully-fledged semantics in terms of the
third layer. We propose a ``\mathwiki'' to\weg{ capitalise on generic}
   harness
Web 2.0 tools and techniques\weg{, harnessing them} to the rich semantics
furnished by contemporary Proof Assistants.

\end{abstract}

\nocite{krowne,flyspeckwiki,lange:swim-demo08}

\section{Background and state of the art}

%
\begin{background}
{We can identify}
\weg{There are, at least for the purposes of this paper,} four worlds of mathematical discourse available on the Web:
\begin{itemize}
\item Traditional mathematical practice: a systematic body of
  knowledge, organised around \weg{papers and book}documents
  \weg{typically }written by expert\weg{ mathematician}s, most often
  in \LaTeX\weg{ but also in other systems like \TeX$_{\rm MACS}$
    \cite{texmacs}}, \weg{with}to varying degrees of
  sophistication\weg{ in markup}.  The intended audience is an expert
readership, and the content is of high quality and reliability, having
been through a rigorous editorial process. Indexing and
cross-referencing is managed externally by journals themselves,
augmented by tools such as CiteSeer\weg{ \cite{citeseer}}, Google Scholar\weg{ \cite{googlescholar}}, and archival sites such as ArXiv\weg{ \cite{arxiv}};
\item \wikipedia, \mathworld, \etc.: universal readership and
  authorship, wide coverage, but relatively shallow and of variable
  reliability, with little systematic development of larger
  theories, and little or no critical gloss on the
  material;\weg{\footnote{Paul Taylor, posting to \texttt{categories}
    mailing list, 2008-03-05}}
\item The Semantic Web, with the OMDoc standard \cite{omdoc}
  and tools like SWiM \cite{lange:swim-demo08}, for organising
  structured documents around a basic notion of ``falling under a
  concept'' (such concepts \weg{typically being}then further organised
  into content dictionaries);
\item The language and (checked) libraries of \emph{proof assistants}, in
  which concepts, definitions, statements, and most importantly,
  \emph{proofs} of theorems are represented in a machine-checkable format.
\end{itemize}
\end{background}
%%%
We focus in this paper on the fourth world, as we expect it to be
least familiar to readers of the paper, but more importantly because
\claim{we believe that proof assistants offer a real, that is to say, formal
\emph{mathematical} semantics to (a Semantic Web of) mathematical
documents.} {Our aim, and that of our partners in a European consortium,
is to integrate all four worlds into a coherent whole, and develop a
``\mathwiki'', a system for the collaborative {authoring and} communication of
computer mathematics to the world.}

%%%\section{State of the Art}
\begin{background}
\paragraph{Proof Assistants}
The basic idea of using computer programs to check mathematical proofs
goes back to the archaeology of {AI} research\weg{ in Artificial Intelligence,
with papers by McCarthy, Newell and Simon's work, etc}. The 
\weg{decisive move was made in the }1960s 
{saw the emergence of two basic paradigms:} de Bruijn's \Automath\ \weg{system}%
\cite{automath}, and Milner's\weg{ elaboration of McCarthy's ideas in the}
\weg{Stanford (and later, Edinburgh) }LCF\weg{ system}.
%%%
\weg{In each \weg{case}system, the basic activity of the human author
  of a proof is to interact with a machine that not only checks
  definitions for well-formedness, but excludes faulty or otherwise
  fallacious reasoning:
%by the use of \emph{types}
in the case of LCF, \weg{using} the type system of the host
programming language \weg{(what eventually became Standard ML)}
\weg{to} control{s} how values of an \emph{abstract} datatype
\texttt{thm} of theorems \weg{could}can be constructed\weg{ in a
  general-purpose programming language}, and in the case of \weg{de
  Bruijn's various systems}\Automath, by \weg{the use of}using
(dependently-typed) \ensuremath{\lambda}-calculus as \weg{the}a
uniform language for definitions and proofs.}
%%%
Both provide highly generic foundational approaches to representing
mathematics: \weg{namely in terms of}as a series of checked objects
(definitions etc.) extending a body of \weg{mathematical }knowledge from an
initial axiomatisation (e.g. of arithmetic or set theory). In \weg{the
  case of }LCF\weg{ approaches,} the objects, including proofs of
their properties, are obtained by running programs to produce values
of {an abstract data}type \texttt{thm}, that is to say they are
\emph{ephemeral} phenomena associated to the persistent program texts
which give rise to them. In \Automath, the objects --- \ensuremath{\lambda}-terms
{in a dependently-typed language uniformly representing definitions and proofs}
--- are themselves persistent\weg{, being simply \lambdaterms,} and in
principle may be independently rechecked, or otherwise \weg{re-}processed.

Modern systems have elaborated these ideas with great sophistication,
extensive libraries, and highly non-trivial formalisations:
%%%
\begin{itemize}
\item The HOL Light system \cite{hollight} is%
\weg{Harrison's re-implementation of Gordon's HOL system \cite{hol}, } 
  an LCF-style
  checker for \weg{Church's simple type theory for }higher-order
  logic; Harrison recently announced a proof of the analytic Prime
  Number Theorem;
\item The Isabelle system \cite{isabelle} is also LCF\weg{ in
    implementation architecture}-like, but adds a generic twist in
  terms of an \Automath-like theory of representation: it is a
  \emph{logical framework}, that is, it is generic over the underlying
  choice of logic and axiomatisation. It is available with libraries
  for both higher-order logic, and for ZF set theory. It has been used
  to formalise G\"odel's completeness theorem, \weg{G\"odel's theorem
  about }the consistency of the axiom of choice, the Prime Number
  Theorem, etc.;
\item The Coq system \cite{coqman} is type-theoretic\weg{ in its foundations}, within
  which objects and proofs are \lambdaterm s in a calculus of
  inductive and coinductive definitions; a notable development is
  Gonthier's formalisation of the \nocomment[Seymour and Robertson
  proof of the] Four Colour Theorem \cite{4color};
\item The Mizar system \cite{mizar}, a proof checker for a strong version of
  set theory, \weg{with the }emphasis{es} \weg{on the }develop\weg{ment of}ing a formalised
  library of standard, classical mathematics.
\end{itemize}
\end{background}

\weg{
\weg{Obviously all this comes}
{There is a definite cost to working with a given proof assistant: }
\weg{at a certain price, which varies from system to system:} 
not least the effort and bureaucracy associated
with producing formal text\weg{ in a formal language}, but usually
also familiarity with the idiom of representation or the proof
metalanguage itself. As a consequence it \weg{really}can take\weg{s} \weg{some
  experience (usually months if not years)} months if not years of
experience to become able to carry out interesting proofs with
reasonable effort. Each system moreover has a bespoke notion of
rendering of the user's formal activity into human-readable form; some
also have \weg{additional} mechanisms for notational convenience in
the formal language, and for avoiding a procedural\weg{, task-oriented}
approach in favour of a declarative language, supporting a more
``natural'', if stilted and verbose, mathematical style of proof.
}

\begin{evaluation}
\claim{The decisive semantic advantage of all these systems over existing
approaches to mathematical documents comes from the infrastructure
of a formalised meta-level: names and binding to support
substitutive definitions, definitional equality, hypothetical and
general reasoning.} The Proof Assistant and \weg{the }Semantic Web
communities \weg{appear}seem to differ over what constitutes a (mathematical)
definition:
\begin{itemize}
\item in the Semantic Web a definition is a reference to a (canonical)
  textual description of the defined object; while
\item for the proof assistant community a definition is a binding with a
  dynamic semantics given by a substitutive notion of
  \emph{definitional equality}, namely the replacement of the named
  object (\textit{definiendum}) by a body (\textit{definiens}).
\end{itemize}
\end{evaluation}

\weg{Again, each proof assistant expresses these concepts in different
ways, but a simple illustration in terms of \weg{a single rule of inference,}
\textit{modus ponens} makes this clear: it is valid to conclude the formula \(C\) from hypotheses \(A\) and \(B\) if we know that
\begin{itemize}
\item \(B\) \emph{is equal to} a formula \(A' \Rightarrow C'\), where
\item \(A\) \emph{is equal to} the formula \(A'\), and
\item \(C\) \emph{is equal to} the formula \(C'\).
\end{itemize}
}

%\nocomment[{
%proof assistants: high level of precision and reliability
%  small user community
%  significant results: fundamental theorems of calculus and algebra, prime number theorem (both elementary and analytic proofs), jordan curve theorem, four color theorem, flyspeck
%  high promise
%}]


\nocomment[\section{some unfinished garbage} {\it
In this paper, we focus on the fourth world, namely that of proof
assistants; as we expect it to be least familiar to readers of this paper.

Proof assistant offer a mechanical framework in which to do mathematics, (i.e. compute and check proofs) and they are designed precisely to offer a direct correspondence between the user's input and the theoretical objects from that framework.

.They provide a precise (i.e. computable) notion of what a definition is, of what a proof is.

Obviously this comes at the price of introducing some bureaucracy in what the user is required to type, and as a consequence it really takes some experience (usually months if not years) to become able to carry out interesting proofs with a reasonable effort.

However, proof assistant

They do, however, have the infrastructure of a formalised meta-level:
substitutive definitions, definitional equality.They provide a precise (i.e. computable) notion of what a definition is, of what a proof is.


W
why the semantic web community needs us:
  framework for making sense out of things, for semantics

  not only making sense of a mathematical expression in a text
  but also of relations between those expressions
  -> contextual reasoning under hypotheses

  framework for both algorithms and proofs




structure versus semantics
  semantic web: lots of structure, but what does it mean?
  proof assistant: even more structure, formal explicit explanation of the meaning
}]

\section{A project proposal: {\mathwiki}}
\weg{Our aim, and that of our partners in a European consortium,
is to integrate all four worlds into a coherent whole, and develop a
``\mathwiki'', a system for the collaborative {authoring and} communication of
computer mathematics to the world. }

% mathwiki project:
%   combines two main parts:
%   - a wikipedia-like encyclopedia of mathematical notions and results
%   - a web-based world-wide integrated formal environment for
%     collaboratively working with many proof assistants

% results can be both:
%   - informal English text
%   - formally checked proof assistant input

% mathwiki will make it easy to integrate more systems into the framework

% mathwiki will contain all the large formal libraries already out there
%   (coq contribs, afp for isabelle, etc.)

\begin{scenario}
 The {\mathwiki} project proposes to combine a Wikipedia-like encyclopedia of
mathematical notions and results, with a web-based integrated formal
environment for collaboratively working with multiple proof
assistants. \claim{Wikipedia has shown that it is possible to create large
bodies of coherent knowledge, by providing lightweight (web-based)
functionality to add material.} In the {\mathwiki} project we similarly
want to provide lightweight web-based functionality to contribute to a
repository of formalised mathematics. This should provide both a means
to do large joint formalisations in a distributed way, but also the
means to search and retrieve material, both at a low level, in terms
of proof assistant-specific \weg{computer code}text, and at the high level of
standard mathematical documents.

\begin{figure}[htb]
\begin{center}
\includegraphics[width=\textwidth]{MathWiki}
\end{center}
\caption{\label{fig.mathwiki}An example MathWiki page for the binomial coefficient }
\end{figure}
%%%\footnotetext{}

The {\mathwiki} repository will include knowledge about mathematical
concepts by the means of high level concept description pages. Those
pages will include links to pages containing the finer details, which
are, in the end, checked proof assistant
code.
We plan to directly incorporate into our project a certain number of
state-of-the-art proof assistants. But the MathWiki itself will be open
to other systems and it should be easy to incorporate
them.
The repository will contain all the large libraries of formal mathematics
that already exist for the included proof assistants, like the Coq
user contributions (\textit{contribs}) and the Archive of Formal Proofs for Isabelle, in order to facilitate access to them.

We have created a prototype \cite{mathwiki} that only supports Coq
(without any semantic aspects yet), which suggests the
project is technically feasible.  In Figure~\ref{fig.mathwiki} we
sketch how the eventual system might look\weg{\footnote{The image }}{ (including
  quoted material from Wikipedia for illustrative purposes). }
\end{scenario}

\begin{evaluation}
Our first claim is that \claim{a mathematical semantic web where the
mathematical notions refer to objects with a real formal semantics in
a proof assistant will be profitable for users of mathematics because
it improves preciseness and correctness.}  Our planned {\mathwiki}
system should substantiate that claim and open up to a wider community
the rich collections of knowledge stored in the repositories of proof
assistants and to facilitate the extension and editing of these
repositories by outside users. 


Our second claim is that \claim{the ``medium'' of {\em computer checkable
  formal proofs\/} will become a valuable asset in ICT, notably in
verification and correctness of software and systems.} At this moment
there is not {\em one\/} type of medium for computer checkable formal
proofs: basically each proof assistant has its own ``media type''. We
think that \claim{in the future these media types will more and more converge
and become exchangeable.} A real mathematical semantic web is the
platform for studying, comparing and exchanging these media types.
\end{evaluation}


\section{Why now: QED 15 years later?}

\begin{discussion}
The motivation for initiating this project precisely now is the
convergence of several decisive factors. One of them is the success of
the Wiki approach in general, and mostly the success of its
application to the encyclopedic endeavour. This example shows that \claim{the
collaborative approach is a good way of developing bodies of shared
knowledge.}

Another key factor is the availability of \weg{several }mature proof
assistants with solid reputations and a certain quantity of formal
developments. \claim{These proof assistants are way past toy
examples and now allow outstanding results;} they can handle large
developments spanning hundreds of files.


Semantic web techniques \weg{are }now available \weg{to }provide a relevant
presentation layer to the user. Although formal proofs are highly
structured and hence easy to index, it is this \weg{very }extremely precise
structure that can \weg{make}leave the user \weg{feel }lost in \weg{too much}the detail{s}, or
unable to \weg{find what she looks for because of too specific search
criteria}search or browse effectively.

The last key element we wish to stress is the availability of Web 2.0
technologies, which support the creation of web-based complex user
interfaces. These technologies are important for our project since interactive
proof development is by far the most popular way of using proof
assistants.

%There are also serious reasons for not having considered this project
%feasible or interesting before.

Already in 1993 the authors of the QED Manifesto \cite{qed} had this
vision: to let the whole world participate in creating a shared
repository of formalised mathematics. We can speculate as to\weg{reasons}
why this was an idea before its time\weg{.}: 
%%%
%%%There was a philosophical disagreement on which system is the best.
%%%
%%%
inevitably, user communities around each system felt keenly the
supposed strengths of their own approach, and the perceived
deficiencies of others'. The relative maturity of \weg{both the }systems and
their libraries has greatly mitigated this state of affairs.

\nocomment[{The first reason is the division of the proof assistant community into user
bases for their preferred system, each of which are strongly
supportive of its design choices. The emphasis on differences between
these tools was encouraged by the quest for survival. This competition
led to separate communities which have now reached a critical mass, so
the focus is now turning to improving communication between different
proof approaches.}]

%Freek: Maybe leave out
\weg{The division also happened because of strongly held opinions among the
community as to the one true \emph{ideal
  foundational framework}. Unfortunately, people do not agree on which
one it might be, or on whether it already has been discovered. Some
research groups go on developing new foundational systems while others
\weg{try to actually} work with what they have (most of them actually do a
little of both).}

The difficulty of formal proof also restrained the ambition of\weg{ the}
proof projects attempted, but with eyes on a bigger prize, collective
development has become common practice in the formal proof community.
This is how the biggest achievements were possible. Mizar and its MML
are the primary example of the success of collective development
though not very focused. More focused examples are the CompCert
project in which a whole team participated in the verification of a C
compiler and the Nijmegen\weg{ Foundation Group's} repository of formalised
mathematics (CoRN) \cite{corn}. The ongoing Flyspeck project
\cite{flyspeck} is another instance.

Proof assistants proposed to be part of the {\mathwiki} project in the
initial phase
are Coq, Isabelle and Mizar. They cover three different foundational
theories (Type Theory, Higher-Order Logic and Set Theory), and embrace
classical as well as intuitionistic mathematics. They also have three
different interaction modes: de Bruijn style, LCF-style and
batch-mode interaction. Thus \claim{the three of them provide an excellent coverage
of the variety among existing proof assistants.}%
\end{discussion}

%initial proof assistants selected for mathwiki project:
%  Coq, Isabelle, Mizar
%  reasons: foundational variety, variety in interaction style
%    convex hull of these systems cover most systems
%  each has its own bespoke document preparation, tool set for browsing


%%% \section{Introduction}

%%% Existing mathematics on the Web --- the mathematics one finds in Wikipedia etc. is deficient in form
%%% and content, never mind in semantics.

%%% Existing mathematics on the Semantic Web is markup- and
%%% content-rich, but sets a high bar for participation from the
%%% non expert user, but expert mathematicians.

%%% Existing proof assistants have a well worked out semantics for
%%% mathematics: definitions, proofs, \ldots, but have an even a higher
%%% bar to adoption.

%%% They do, however, have the infrastructure of a formalised meta-level:
%%% substitutive definitions, definitional equality.

%%% --

%%% The two communities have however different understanding of
%%% what constitutes  a definition. For the Semantic Web a definition
%%% is a reference to a (canonical) textual description of the defined
%%% object.

%%% For the proof assistant community a definition is binding with a
%%% dynamic semantics given by a substitutive notion of
%%% \emph{definitional equality}, namely the replacement of the named
%%% object (\textit{definiendum}) by a body (\textit{definiens}). This
%%% arises in a variety of ways in different proof assistants.


%%% --

%%% In \textsc{HOL Light} all definitions are replaced with their ...
%%% In type theory...
%%% Redefinitions in Mizar.

%%% --

%%% The activity of putting mathematics on the web should not only be
%%% about presentation of existing mathematical practice but should
%%%  also embrace the emerging paradigm of computer mathematics based
%%% on proof assistant technology, namely:

%%% The key advance is not only the representation of concepts, but of
%%% relationships between them expressed in algorithms and proofs. That
%%% is, we have a \emph{mathematical} semantics for mathematical concepts.

%%% --

%%% We describe a web-based system that should combine high-level
%%% descriptions of mathematical concepts with detailed semantical
%%% descriptions of these same concepts in a \PA. The system should have
%%% different functionalities. First of all, functionality of \wikipedia,
%%% providing high level descriptions of mathematical concepts and the
%%% possibility for users to contribute via a simple interface. Second,
%%% the functionality of formalizing mathematics through a
%%% web-interface. This formalized mathematics can then be ``linked to''
%%% the high-level informal description, thus providing access to
%%% formalized mathematics through high level \wikipedia-like pages.

%%% So, all together, the system we envisage is at the same time
%%% \begin{itemize}
%%% \item
%%% a web-interface to proof assistants,
%%% \item
%%% a respository of formalized mathematics,
%%% \item
%%% a \wiki\ system for mathematical information,
%%% \item
%%% a web-based system to create semantic links between mathematical
%%% notions described on various levels of formal detail.
%%% \end{itemize}

%%% So, the system should integrate the properties of \wiki's with proof
%%% assistants. In proof assistants, the mathematics has a very precise
%%% and formal meaning and this semantics naturally provides links between
%%% different notions, e.g.\ from a definition of a concept to the
%%% definitions of the concepts in terms of which it is defined. However,
%%% there are many more links between mathematical concepts, e.g.\ concept
%%% that are ``related'', or ``similar''. These links should be provided
%%% by a knowledgeable user, which is dome in a \wiki\ system by providing
%%% a hyperlink.


\section{Conclusion}

\begin{conclusion}
The power of Wiki technology is to make building a new encyclopedia of
mathematics a truly global democratic enterprise.
Contemporary proof assistant technology has reached the point where we
can imagine such a richly structured web of mathematics with a fully-fledged
semantics in a formal system. \claim{A real Semantic Web for mathematics deserves
a real semantics.}
\end{conclusion}

%\subsection{Wikipedia}
%A {joint} {distributed} development of a {coherent} {on-line} encyclopedia.\\
%``{Doesn't work in theory \ldots but works in practice}''

%\begin{itemize}
%\item Claim 1
%The Wikipedia approach also works for semantically rich (very structured) data.\\
%
%{Consistency} Issues!

%\item Claim 2
%We can create attractive, useful web-pages for mathematical notions
%with formal content.
%\end{itemize}

\nocomment[{
\section{References}

Matita \cite{matita},
PVS \cite{pvs},
NuPrl \cite{nuprl}

Lamport \cite{lamport}
}]

%\bibliographystyle{plain}
%\bibliography{t}

\begin{thebibliography}{10}

\bibitem{qed}
R.~Boyer et~al.
\newblock {The QED Manifesto}.
\newblock In Bundy, ed., {\em Automated Deduction -- CADE 12}, 
  {\em LNAI} 814. Springer, 1994.

\bibitem{openmath}
S.~Buswell, O.~Caprotti, D.P. Carlisle, M.C. Dewar, M.~Ga{\"e}tano, and
  M.~Kohlhase.
\newblock {The OpenMath Standard, version 2.0}, 2002.

\bibitem{coqman}
{Coq Team}.
\newblock {\em The Coq Proof Assistant Reference Manual V8.1}.
\newblock INRIA, 2006.

\bibitem{mathwiki}
P.~Corbineau and C.~Kaliszyk.
\newblock Cooperative repositories for formal proofs.
\newblock In Kauers \textit{et al.}  eds., {\em
  Calculemus/MKM},  {\em LNCS} 4573. Springer, 2007.
%%%, Kerber, Miner, and Windsteiger,

\bibitem{corn}
L.~Cruz-Filipe, H.~Geuvers, and F.~Wiedijk.
\newblock {C-CoRN}, the constructive {Coq} repository at {Nijmegen}.
\newblock In Asperti \textit{et al.} eds., {\em MKM},
   {\em LNCS} 3119. Springer, 2004.
%%%, Bancerek, and Trybulec,

\bibitem{4color}
G.~Gonthier.
\newblock {A computer-checked proof of the Four Colour Theorem}, 2006.

\bibitem{flyspeck}
T.~C. Hales.
\newblock Introduction to the flyspeck project.
\newblock In Coquand \textit{et al.} eds., {\em Mathematics,
  Algorithms, Proofs},  {\em Dagstuhl Proceedings} 05021.
  IBFI, Germany, 2005.
%%%, Lombardi, and Roy,
%%% Schloss Dagstuhl

\bibitem{hollight}
J.~Harrison.
\newblock {HOL} light: A tutorial introduction.
\newblock In Srivas and Camilleri, eds., {\em Proceedings of {FMCAD}'96},  {\em LNCS} 1166. Springer, 1996.

\bibitem{omdoc}
M.~Kohlhase.
\newblock {\em OMDoc - An Open Markup Format for Mathematical Documents
  [version 1.2]},  {\em LNCS} 4180.
\newblock Springer, 2006.

\bibitem{krowne}
A.P. Krowne.
\newblock An architecture for collaborative math and science digital libraries.
\newblock Master's thesis, Virginia Tech Dept.\ of Computer Science,
  Blacksburg, VA, 2003.

\bibitem{lange:swim-demo08}
C.~Lange.
\newblock {SWiM} -- a semantic wiki for mathematical knowledge management.
\newblock In Bechhofer \textit{et al.} eds., {\em ESWC},  {\em LNCS} 5021. Springer, 2008.
%%%, Hauswirth, Hoffmann, and Koubarakis,

\bibitem{flyspeckwiki}
C.~Lange, S.~McLaughlin, and F.~Rabe.
\newblock Flyspeck in a semantic wiki.
\newblock Unpublished.

\bibitem{mizar}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, 1993.

\bibitem{ned:geu:vri:94}
R.P. Nederpelt, J.H. Geuvers, and R.C. de~Vrijer.
\newblock {\em Selected Papers on Automath},  {\em Studies in
  Logic and the Foundations of Mathematics} 133.
\newblock Elsevier, 1994.

\bibitem{isabelle}
T.~Nipkow, L.~C. Paulson, and M.~Wenzel.
\newblock {\em Isabelle/HOL - A Proof Assistant for Higher-Order Logic},  {\em LNCS} 2283.
\newblock Springer, 2002.

\bibitem{automath}
D.T. van Daalen.
\newblock {A description of Automath and some aspects of its language theory}.
\newblock In Nederpelt et~al. \cite{ned:geu:vri:94}.
\newblock Article A.3.

\bibitem{wiedijk06-17provers}
F.~Wiedijk, ed.
\newblock {\em The Seventeen Provers of the World}, {\em LNCS} 3600.
\newblock Springer, 2006.

\end{thebibliography}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: