Changeset 3516
 Timestamp:
 Nov 17, 2014, 12:08:32 PM (5 years ago)
 Location:
 Papers/jarassembler2014
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarassembler2014/boenderjar2014.bib
r3514 r3516 10 10 } 11 11 12 @inproceedings 13 { bove:brief:2009, 14 author = {Ana Bove and Peter Dybjer and Ulf Norell}, 15 title = {A Brief Overview of {Agda}  A Functional Language with Dependent Types}, 16 booktitle = {Theorem Proving in Higherorder Logics {(TPHOLs)}}, 17 year = {2009} 18 } 19 20 @manual 21 { coq:2004, 22 title = {The {Coq} proof assistant reference manual}, 23 author = {{The Coq development team}}, 24 organization = {{LogiCal Project}}, 25 note = {Version 8.0}, 26 year = {2004}, 27 url = {http://coq.inria.fr} 28 } 29 12 30 @misc 13 31 { cerco:2011, 
Papers/jarassembler2014/boenderjar2014.tex
r3515 r3516 14 14 \usepackage{kpfonts} 15 15 \usepackage[T1]{fontenc} 16 \usepackage[ttdefault=true]{AnonymousPro} 17 18 \newcommand{\deffont}[1]{\textbf{#1}} 16 19 17 20 \bibliographystyle{alpha} 18 21 19 \renewcommand{\verb}{\lstinline}22 %\renewcommand{\verb}{\lstinline} 20 23 \def\lstlanguagefiles{lstgrafite.tex} 21 24 \lstset{language=Grafite} … … 53 56 \label{subsect.matita} 54 57 55 Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.56 It features full spectrum dependent types as well as a sophisticated system of coercions, both of which we exploit in this formalisation.57 58 Matita's syntax should be familiar for those readers acquainted with the OCaml functional programming language.59 Nevertheless, we provide a brief summary of the main syntactic features of Matita:58 Matita is a theorem prover based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. 59 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 in this paper. 60 61 Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml. 62 Nevertheless, we provide a brief explanation of the main syntactic and typetheoretic features of Matita that will be needed to follow the body of the paper: 60 63 \begin{itemize} 61 64 \item 62 Nonrecursive definitions are introduced with the \texttt{definition} keyword, and recursive definitions with the \texttt{let rec} keywords. 63 \item 64 There is extensive provision for customising syntax (through Unicode). Matita has an advanced system of overloading and resolution so that definitions and proofs look as natural as possible. 65 Nonrecursive functions and definitions are introduced via the \texttt{definition} keyword, whilst recursive functions are introduced with \texttt{let rec}. 66 Mutually recursive functions are separated via the \texttt{and} keyword. 67 \item 68 Matita has an infinite hierarchy of type universes. 69 A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy. 70 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}. 71 Matita, unlike Coq~\cite{coq:2004} or Agda~\cite{bove:brief:2009}, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead. 72 \item 73 Matita's type theory plays host to a rich and expressive higherorder logic. 74 Constant \texttt{True} and \texttt{False} represent truth and (constructive) falsity in \texttt{Prop} respectively. 75 Inductive families in \texttt{Prop} encode conjunction and disjunction$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectivelyalso. 76 As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$type). 77 \item 78 Inductive families are introduced via the \texttt{inductive} keyword with named constructor declarations separated with a bar. 79 Mutually inductive data family declarations are separated via \texttt{with}. 80 \item 81 Records are introduced with the \texttt{record} keyword. 82 A Matita record 83 \begin{lstlisting} 84 record R : Type[0] := { F1 : nat }. 85 \end{lstlisting} 86 may be thought of as syntactic sugar for a singleconstructor inductive data type of the same name: 87 \begin{lstlisting} 88 inductive R : Type[0] := 89  mk_R : nat > R. 90 \end{lstlisting} 91 In particular, declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect. 92 \deffont{Projections}, one for each of the record's fields, are also registered in the global context. 93 In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection. 94 95 Record fields may be marked as coercions. 96 In the following example 97 \begin{lstlisting} 98 record S : Type[1] := 99 { 100 Carrier :> Type[0]; 101 op : Carrier > Carrier > Carrier 102 } 103 \end{lstlisting} 104 the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}', and the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita's typechecker, thus facilitating the common mathematical practice of confusing a mathematical structure with its underlying carrier set. 105 \item 106 There is provision for customising syntax (through Unicode). 107 Matita has a typedirected system of overloading and resolution so that definitions and proofs look `natural'. 65 108 \end{itemize} 66 109
Note: See TracChangeset
for help on using the changeset viewer.