Changeset 1020
 Timestamp:
 Jun 21, 2011, 12:09:33 PM (9 years ago)
 Location:
 src/ASM/CPP2011
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.bib
r981 r1020 218 218 219 219 } 220 221 @inproceedings{russell, 222 author = {Matthieu Sozeau}, 223 title = {Subset Coercions in {C}oq}, 224 booktitle = {Types for Proofs and Programs}, 225 series = {LNCS}, 226 year = {2006}, 227 pages = {237252}, 228 VOLUME = {4502/2007}, 229 PUBLISHER = {SpringerVerlag}, 230 doi = {10.1007/9783540744641\_16}, 231 } 
src/ASM/CPP2011/cpp2011.tex
r1019 r1020 191 191 In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness. 192 192 193 The rest of this paper is a detailed description of our proof. 193 The rest of this paper is a detailed description of our proof that is partly 194 still in progress. 194 195 195 196 %  % … … 208 209 \label{sect.matita} 209 210 210 Matita is a proof assistant based on the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. 211 For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar. 212 However, we take time here to explain one of Matita's syntactic idiosyncrasies. 213 The use of `$\mathtt{?}$' or `$\mathtt{\ldots}$' in an argument position denotes a term or terms to be inferred automatically by unification, respectively. 214 The use of `$\mathtt{?}$' in the body of a definition, lemma or axiom denotes an incomplete term that is to be closed, by hand, using tactics. 211 Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. In particular, it features dependent 212 types that we heavily exploit in the formalization. The syntax of the 213 statements and definitions in the paper should be selfexplanatory, at least 214 to those exposed to dependent type theory. We only remark the use of 215 of `$\mathtt{?}$' or `$\mathtt{\ldots}$' for omitting single terms or 216 sequences of terms to be inferred automatically by the system, respectively. 217 Those that are not inferred are left to the user as proof obligations. 218 Pairs are denoted with angular brackets. 219 220 Matita features a liberal system of coercions. In particular, it is possible 221 to define a uniform coercion $\lambda x.\langle x,?\rangle$ from every type $T$ to the dependent product $\Sigma x:T.P~x$. The coercion opens a proof 222 obligation that asks the user to prove that $P$ holds for $x$. When a coercion 223 must be applied to a complex term (a lambdaabstraction, a local definition, 224 a case analysis), the system automatically propagates the coercion to the 225 subterms. For instance, to apply a coercion to force $\lambda x.M : A \to B$ 226 to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from 227 $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. This is 228 significant when the coercion opens a proof obligation, since the user 229 will be presented with multiple, but simpler proof obligations in the right 230 context. Matita supports in this way the proof methodology developed by 231 Sozeau in~\cite{russell}, but with an implementation that is lighter than the 232 one of Coq and more integrated in the system. 215 233 216 234 %  %
Note: See TracChangeset
for help on using the changeset viewer.