Changeset 1845 for Deliverables/D1.2
- Timestamp:
- Mar 15, 2012, 2:14:54 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/Presentations/WP3.tex
r1836 r1845 1 1 \documentclass[nopanel]{beamer} 2 \usepackage{graphicx,color} 2 3 3 4 \usetheme{Frankfurt} … … 19 20 %\SetUnicodeOption{postscript} 20 21 %\usepackage{hyperref} 21 \usepackage{graphicx,color}22 22 \usepackage{latexsym} 23 23 \usepackage{listings} … … 213 213 214 214 \red{Instead}: recursive `coerce to desired type' approach.\\ 215 (Doesn't get some things, 216 e.g., \lstinline'==') 217 % TODO: would like to separate, show example properly, note proofs 215 % (Doesn't get some things, 216 % e.g., \lstinline'==') 218 217 \end{frame} 219 218 … … 238 237 } 239 238 240 % \frame{241 % \frametitle{Clight: adding runtime functions}242 243 % Replaces ops not supported by target with function calls.244 245 % \begin{itemize}246 % \item Add functions as Clight ASTs (rather than prototype's reparsing approach)247 % \item substituting function calls is horrible248 % \begin{itemize}249 % \item Clight does not permit calls in expressions250 % \item Need to add statements in front of the target expression251 % \item Messy, duplication252 % \item Hard: just noticed that even the prototype gets it wrong253 % \end{itemize}254 % \item Implemented, but\dots255 % \end{itemize}256 257 % \textsc{Proposal}: shift to later in the compilation process258 % \begin{itemize}259 % \item easy substitution260 % \item adjust semantics to emit extra cost labels261 % \item get to use lower level features262 % \end{itemize}263 % }264 239 \section{Cminor} 265 240 \begin{frame}[fragile] … … 272 247 \end{itemize} 273 248 274 % TODO: update!275 249 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] 276 250 inductive expr : typ $\rightarrow$ Type[0] ≝ … … 635 609 636 610 \bigskip 637 It remains to prove that flattening these traces yields the original. 638 } 639 640 % \frame{ 641 % \frametitle{Difficulties with invariants} 642 643 % \begin{itemize} 644 % \item Not clear if we can use Russell 645 % \begin{itemize} 646 % \item Want to use existing proofs rather than generated equalities 647 % \item Some non-uniform treatment of cases 648 % \end{itemize} 649 % \item Stresses Matita somewhat (try forgetting to make something a dependent pair) 650 % \item Lots of fiddly proof obligations that are simple, but a pain to deal with 651 % \begin{itemize} 652 % \item Appeal to monotonicity 3 times, then note that the label was added to the graph here 653 % \end{itemize} 654 % \item Already verbose, yet don't cover globals. 655 % \end{itemize} 656 657 % I'd like to see if better use of Matita's features can help with this stuff. 658 659 % \bigskip 660 % Open to suggestions for better methods. 661 % } 611 Next, prove that flattening these traces yields the original. 612 } 662 613 663 614 \frame{
Note: See TracChangeset
for help on using the changeset viewer.