Changeset 955


Ignore:
Timestamp:
Jun 15, 2011, 12:00:31 PM (8 years ago)
Author:
mulligan
Message:

more work on conclusions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r954 r955  
    170170\label{sect.conclusions}
    171171
    172 \subsection{Use of dependent types}
    173 \label{subsect.use.of.dependent.types}
     172\subsection{Use of dependent types and Russell}
     173\label{subsect.use.of.dependent.types.and.Russell}
    174174
    175 As it stands our use of complex dependent types is limited in the formalisation.
    176 Where it made sense, for example in data structures like tries and vectors, we have made limited use of dependent types.
     175Our formalisation makes sparing use of dependent types.
     176In certain datastructures, such as tries and vectors, they are used to guarantee invariants.
     177However, we have currently shyed away from making extensive use of dependent types and inductive predicates in the proof of correctness for the assembler itself.
     178This is because complex dependent types and inductive predicates tend not to co\"operate particularly well with tactics such as inversion.
     179
     180In their stead, where it makes sense, we used Matita's implementation of Russell~\cite{}.
    177181
    178182\subsection{Related work}
Note: See TracChangeset for help on using the changeset viewer.