Changeset 1190
- Timestamp:
- Sep 5, 2011, 5:53:20 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r1189 r1190 319 319 Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq. 320 320 As 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 thereforetotal.321 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$. 322 Unlike O'Caml, all recursive functions admitted by the Matita typechecker must be structurally recursive and total. 323 323 324 324 We box Matita code to distinguish it from O'Caml code.
Note: See TracChangeset
for help on using the changeset viewer.