Changeset 3518
 Timestamp:
 Nov 18, 2014, 12:25:43 PM (5 years ago)
 Location:
 Papers/jarassembler2014
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarassembler2014/boenderjar2014.bib
r3516 r3518 8 8 issue = {2}, 9 9 year = {2007} 10 } 11 12 @article 13 { sacerdoticoen:tinycals:2007, 14 author = {Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli}, 15 title = {{Tinycals}: Step by Step Tacticals}, 16 journal = {Electronic Notes in Theoretical Computer Science}, 17 volume = {174}, 18 number = {2}, 19 pages = {125142}, 20 doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026}, 21 year = {2007} 22 } 23 24 @inproceedings 25 { asperti:higherorder:2007, 26 author = {Andrea Asperti and Enrico Tassi}, 27 title = {Higher order Proof Reconstruction from ParamodulationBased Refutations: The Unit Equality Case}, 28 booktitle = {Towards Mechanized Mathematical Assistants: Calculemus}, 29 pages = {146160}, 30 series = {Lecture Notes in Computer Science}, 31 volume = {4573}, 32 year = 2007 10 33 } 11 34 
Papers/jarassembler2014/boenderjar2014.tex
r3517 r3518 59 59 \label{subsect.matita} 60 60 61 Matita is a theorem prover based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. 62 The system features a full spectrum of dependent types and (co)inductive families, as well as a sophisticated system of coercions, all of which we exploit in the formalisation described herein. 61 In this Subsection we provide an overview of Matita, the host system for all proofs reported in this paper. 62 63 Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}. 64 The system features a full spectrum of dependent types and (co)inductive families, a sophisticated system of uniform coercions, a tacticdriven proof construction engine~\cite{sacerdoticoen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higherorder:2007} all of which we exploit in the formalisation described herein. 63 65 64 66 Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML, and the type theory that Matita implements is very similar to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}. … … 71 73 \item 72 74 Matita has an infinite hierarchy of type universes. 73 A single \emph{impredicative}universe of types, \texttt{Prop}, exists at the base of this hierarchy.74 An infinite series of \emph{predicative}universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.75 A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy. 76 An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}. 75 77 Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead. 76 78 \item
Note: See TracChangeset
for help on using the changeset viewer.