Index: Papers/jar-cerco-2017/introduction.tex
===================================================================
--- Papers/jar-cerco-2017/introduction.tex (revision 3617)
+++ Papers/jar-cerco-2017/introduction.tex (revision 3618)
@@ -273,6 +273,17 @@
\subsection{Introduction to Matita}
-The theorem prover used to implement the prototype compiler is
-Matita~\cite{matita}.
+The theorem prover used to implement and verify the prototype compiler is
+Matita~\cite{matita}.
+
+Matita, like Coq, is based on the Calculus of (Co)Inductive Constructions. Its
+main features are:
+
+\begin{itemize}
+ \item A bidirectional type inference algorithm, which combines usage of
+ inferred and expected types. The type inference algorithm also uses a hints
+ system that helps with unification;
+ \item A disambiguation system that allows for notation overloading by having
+ the parser and typechecker cooperate closely.
+\end{itemize}
\subsection{Map of the paper}