Changeset 810


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

More added.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r809 r810  
    302302\label{sect.design.issues.formalisation}
    303303
    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$}' denoting an argument or arguments to be inferred, respectively.
     304Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq.
     305Matita's internal language is similar to O'Caml's.
     306The symbols `\texttt{?}' or `\texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively.
    307307
    308308A full account of the formalisation can be found in~\cite{cerco-report:2011}.
Note: See TracChangeset for help on using the changeset viewer.