 Timestamp:
 Mar 6, 2017, 3:50:43 PM (16 months ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarcerco2017/introduction.tex
r3616 r3618 273 273 \subsection{Introduction to Matita} 274 274 275 The theorem prover used to implement the prototype compiler is 276 Matita~\cite{matita}. 275 The theorem prover used to implement and verify the prototype compiler is 276 Matita~\cite{matita}. 277 278 Matita, like Coq, is based on the Calculus of (Co)Inductive Constructions. Its 279 main 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} 277 288 278 289 \subsection{Map of the paper}
Note: See TracChangeset
for help on using the changeset viewer.