Ignore:
Timestamp:
Oct 25, 2012, 12:30:01 PM (7 years ago)
Author:
mulligan
Message:

Some more minor changes

Location:
Papers/polymorphic-variants-2012
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/polymorphic-variants.bib

    r2414 r2416  
     1@article
     2{ asperti:user:2007,
     3  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
     4  title = {User interaction with the {Matita} proof assistant},
     5  journal = {Automated Reasoning},
     6  pages = {109--139},
     7  volume = {39},
     8  issue = {2},
     9  year = {2007}
     10}
     11
    112@inproceedings
    213{ garrigue:code:2000,
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2414 r2416  
    9494\begin{minipage}[b]{0.45\linewidth}
    9595\begin{lstlisting}
     96
    9697\end{lstlisting}
    9798\end{minipage}
     
    123124\subsection{Matita}
    124125\label{subsect.matita}
     126
     127Matita~\cite{asperti:user:2007} is a dependently-typed proof assistant developed in Bologna, implementing the Calculus of (Co)inductive Constructions, a type theory similar to that of Coq.
     128Throughout this paper, all running examples are provided in Matita's proof script vernacular.
     129This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward.
     130
     131One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively.
     132Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.
     133
     134Matita
    125135
    126136\subsection{Subtyping as instantiation vs subtyping as safe static cast}
Note: See TracChangeset for help on using the changeset viewer.