Ignore:
Timestamp:
Sep 5, 2011, 5:53:20 PM (8 years ago)
Author:
mulligan
Message:

improved explanation of matita

File:
1 edited

Legend:

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

    r1189 r1190  
    319319Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq.
    320320As a programming language, Matita corresponds to the functional fragment of O'Caml extended with dependent types.
    321 Matita also features a rich higher-order logic for reasoning about programs.
    322 Unlike O'Caml, all recursive functions must be structurally recursive, and therefore total.
     321Matita also features a rich higher-order logic for reasoning about programs, including a universe hierarchy with a single impredicative universe, \texttt{Prop}, and potentially infinitely many predicative universes \texttt{Type[i]} for $0 \geq i$.
     322Unlike O'Caml, all recursive functions admitted by the Matita typechecker must be structurally recursive and total.
    323323
    324324We box Matita code to distinguish it from O'Caml code.
Note: See TracChangeset for help on using the changeset viewer.