Changeset 1190

Timestamp:

Sep 5, 2011, 5:53:20 PM (8 years ago)

Author:

mulligan

Message:

improved explanation of matita

File:

• Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) (1 diff)

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -319 +319 @@
 Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq.
 As a programming language, Matita corresponds to the functional fragment of O'Caml extended with dependent types.
-Matita also features a rich higher-order logic for reasoning about programs.
-Unlike O'Caml, all recursive functions must be structurally recursive, and therefore total.
+Matita 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$.
+Unlike O'Caml, all recursive functions admitted by the Matita typechecker must be structurally recursive and total.
 
 We box Matita code to distinguish it from O'Caml code.