Changeset 956


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

changes prior to claudio's editing

File:
1 edited

Legend:

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

    r955 r956  
    178178This is because complex dependent types and inductive predicates tend not to co\"operate particularly well with tactics such as inversion.
    179179
    180 In their stead, where it makes sense, we used Matita's implementation of Russell~\cite{}.
     180However, there are certain cases where the use of dependent types is unavoidable.
     181For instance, when proving that the \texttt{build\_maps} function is correct, a function that collates the cost and data labels of an assembly program into map datastructures.
     182In cases such as these we make use of Matita's implementation of Russell~\cite{}.
    181183
    182184\subsection{Related work}
Note: See TracChangeset for help on using the changeset viewer.