# Changeset 3618

Ignore:
Timestamp:
Mar 6, 2017, 3:50:43 PM (6 months ago)
Message:

File:
1 edited

Unmodified
Removed
• ## Papers/jar-cerco-2017/introduction.tex

 r3616 \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}
Note: See TracChangeset for help on using the changeset viewer.