Changeset 3618


Ignore:
Timestamp:
Mar 6, 2017, 3:50:43 PM (8 weeks ago)
Author:
boender
Message:

Added Matita section

File:
1 edited

Legend:

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

    r3616 r3618  
    273273\subsection{Introduction to Matita}
    274274
    275 The theorem prover used to implement the prototype compiler is
    276 Matita~\cite{matita}.
     275The theorem prover used to implement and verify the prototype compiler is
     276Matita~\cite{matita}.
     277
     278Matita, like Coq, is based on the Calculus of (Co)Inductive Constructions. Its
     279main features are:
     280
     281\begin{itemize}
     282        \item A bidirectional type inference algorithm, which combines usage of
     283        inferred and expected types. The type inference algorithm also uses a hints
     284        system that helps with unification;
     285        \item A disambiguation system that allows for notation overloading by having
     286        the parser and typechecker cooperate closely.
     287\end{itemize}
    277288
    278289\subsection{Map of the paper}
Note: See TracChangeset for help on using the changeset viewer.