Changeset 3518


Ignore:
Timestamp:
Nov 18, 2014, 12:25:43 PM (5 years ago)
Author:
mulligan
Message:

little more added

Location:
Papers/jar-assembler-2014
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-assembler-2014/boender-jar-2014.bib

    r3516 r3518  
    88  issue = {2},
    99  year = {2007}
     10}
     11
     12@article
     13{ sacerdoti-coen: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 = {125--142},
     20  doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026},
     21  year = {2007}
     22}
     23
     24@inproceedings
     25{ asperti:higher-order:2007,
     26  author = {Andrea Asperti and Enrico Tassi},
     27  title = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case},
     28  booktitle = {Towards Mechanized Mathematical Assistants: Calculemus},
     29  pages = {146--160},
     30  series = {Lecture Notes in Computer Science},
     31  volume = {4573},
     32  year = 2007
    1033}
    1134
  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3517 r3518  
    5959\label{subsect.matita}
    6060
    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.
     61In this Subsection we provide an overview of Matita, the host system for all proofs reported in this paper.
     62
     63Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}.
     64The system features a full spectrum of dependent types and (co)inductive families, a sophisticated system of uniform coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007} all of which we exploit in the formalisation described herein.
    6365
    6466Matita'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}.
     
    7173\item
    7274Matita 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}.
     75A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
     76An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
    7577Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
    7678\item
Note: See TracChangeset for help on using the changeset viewer.