From 7703897d2b14dd101c763a4aa6d99b7cc95011d1 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 29 Nov 2005 14:22:56 +0000
Subject: [PATCH 1/1] Added a few bibliographic entries.

---
 helm/papers/matita/matita.bib  | 18 ++++++++++++++++++
 helm/papers/matita/matita2.tex | 29 +++++++++++++++--------------
 2 files changed, 33 insertions(+), 14 deletions(-)

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 5b53ac0b9..4927850ba 100644
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -938,6 +938,13 @@
  key = "ALF"
 }
 
+@misc{CoqManual,
+ title = "The {C}oq Proof Assistant Reference Manual",
+ author = "The Coq Development Team",
+ howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
+ key = "CoqManual"
+}
+
 @misc{Coq,
  title = "The {C}oq proof-assistant",
  howpublished = "\\\url{http://coq.inria.fr}",
@@ -976,6 +983,17 @@
  key = "Isabelle"
 }
 
+@book{nuprl-book,
+  author =    "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and 
+               W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and 
+               T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
+               Scott F. Smith",
+  title =     "Implementing Mathematics with the {N}uprl Development System",
+  publisher = "Prentice-Hall",
+  year =      1986,
+  address =   "NJ"
+}
+
 @misc{nuprl,
  title = "The {NuPRL} proof-assistant",
  howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}",
diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 77b7c1406..69e9d06a0 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -118,22 +118,21 @@ Digital Libraries}
 
 \section{Introduction}
 \label{sec:intro}
-In this paper we describe the architecture and a few distintive features of the
-\emph{\MATITA} proof assistant. \MATITA{} was not conceived out of the blue
-one single day; it has been the next natural step in the evolution of one
-line of research we started six years ago. Thus, to better understand the
-system, we start from its historical roots.
+\MATITA{} is the Proof Assistant under development by the \HELM{} team
+\cite{mkm-helm} at the University of Bologna, under the direction of 
+Prof.~Asperti. \\
+The paper describes the overall architecture of
+the system, focusing on its most distintive and innovative 
+features.
 
 \subsection{Historical Perspective}
-\MATITA{} is under development by the \HELM{} team
-\cite{mkm-helm} at the University of Bologna, under the direction of 
-Prof.~Asperti. 
-The origin of the system goes back to 1999. At the time we were mostly 
+The origins of \MATITA{} go back to 1999. At the time we were mostly 
 interested to develop tools and techniques to enhance the accessibility
 via Web of formal libraries of mathematics. Due to its dimension, the
-library of the \COQ{} proof assistant (of the order of 35'000 theorems) 
+library of the \COQ{}\cite{CoqManual} proof assistant (of the order of 35'000 theorems) 
 was choosed as a privileged test bench for our work, although experiments
-have been also conducted with other systems, and notably with \NUPRL{}.
+have been also conducted with other systems, and notably 
+with \NUPRL{}\cite{nuprl-book}.
 The work, mostly performed in the framework of the recently concluded 
 European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the 
 following teps:
@@ -165,7 +164,8 @@ At the end of the \MOWGLI{} project we already disposed of the following
 techniques and libraries:
 \begin{itemize}
 \item XML specifications for the Calculus of Inductive Constructions,
-with libraries for parsing and saving mathematical objects in such a format;
+with libraries for parsing and saving mathematical objects in such a format
+\cite{exportation-module};
 \item metadata specifications with libraries for indexing and querying the
 XML knowledge base;
 \item a proof checker library (i.e. the {\em kernel} of a proof assistant), 
@@ -177,8 +177,9 @@ mathematical notation \cite{disambiguation};
 \item a {\em refiner} library, i.e. a type inference system, based on
 partially specified terms, used by the disambiguating parser;
 \item complex transformation algorithms for proof rendering in natural
-language;
-\item an innovative rendering widget, supporting high-quality bidimensional
+language \cite{remathematization};
+\item an innovative rendering widget \cite{padovani}, supporting 
+high-quality bidimensional
 rendering, and semantic selection, i.e. the possibility to select semantically
 meaningful rendering expressions, and to past the respective content into
 a different text area.
-- 
2.39.2