# Changeset 810 for Deliverables

Ignore:
Timestamp:
May 16, 2011, 5:12:16 PM (9 years ago)
Message:

 r809 \label{sect.design.issues.formalisation} We typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}}. Matita's syntax is straightforward if familiar with Coq or O'Caml. One subtlety is the use of \texttt{?}' or \texttt{$\ldots$}' denoting an argument or arguments to be inferred, respectively. Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq. Matita's internal language is similar to O'Caml's. The symbols \texttt{?}' or \texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively. A full account of the formalisation can be found in~\cite{cerco-report:2011}.