Changeset 810 for Deliverables/D4.1/ITPPaper/itp2011.tex
 Timestamp:
 May 16, 2011, 5:12:16 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r809 r810 302 302 \label{sect.design.issues.formalisation} 303 303 304 We typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}}.305 Matita's syntax is straightforward if familiar with Coq or O'Caml.306 One subtlety is the use of `\texttt{?}' or `\texttt{$\ldots$}' denotingan argument or arguments to be inferred, respectively.304 Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq. 305 Matita's internal language is similar to O'Caml's. 306 The symbols `\texttt{?}' or `\texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively. 307 307 308 308 A full account of the formalisation can be found in~\cite{cercoreport:2011}.
Note: See TracChangeset
for help on using the changeset viewer.