# Changeset 1845 for Deliverables

Ignore:
Timestamp:
Mar 15, 2012, 2:14:54 PM (8 years ago)
Message:

Minor WP3 revisions prior to more major stuff.

File:
1 edited

### Legend:

Unmodified
 r1836 \documentclass[nopanel]{beamer} \usepackage{graphicx,color} \usetheme{Frankfurt} %\SetUnicodeOption{postscript} %\usepackage{hyperref} \usepackage{graphicx,color} \usepackage{latexsym} \usepackage{listings} \red{Instead}: recursive `coerce to desired type' approach.\\ (Doesn't get some things, e.g., \lstinline'==') % TODO: would like to separate, show example properly, note proofs % (Doesn't get some things, % e.g., \lstinline'==') \end{frame} } % \frame{ % \frametitle{Clight: adding runtime functions} % Replaces ops not supported by target with function calls. % \begin{itemize} % \item Add functions as Clight ASTs (rather than prototype's reparsing approach) % \item substituting function calls is horrible % \begin{itemize} % \item Clight does not permit calls in expressions % \item Need to add statements in front of the target expression % \item Messy, duplication % \item Hard: just noticed that even the prototype gets it wrong % \end{itemize} % \item Implemented, but\dots % \end{itemize} % \textsc{Proposal}: shift to later in the compilation process % \begin{itemize} % \item easy substitution % \item adjust semantics to emit extra cost labels % \item get to use lower level features % \end{itemize} % } \section{Cminor} \begin{frame}[fragile] \end{itemize} % TODO: update! \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt] inductive expr : typ $\rightarrow$ Type[0] ≝ \bigskip It remains to prove that flattening these traces yields the original. } % \frame{ % \frametitle{Difficulties with invariants} % \begin{itemize} % \item Not clear if we can use Russell % \begin{itemize} % \item Want to use existing proofs rather than generated equalities % \item Some non-uniform treatment of cases % \end{itemize} % \item Stresses Matita somewhat (try forgetting to make something a dependent pair) % \item Lots of fiddly proof obligations that are simple, but a pain to deal with % \begin{itemize} % \item Appeal to monotonicity 3 times, then note that the label was added to the graph here % \end{itemize} % \item Already verbose, yet don't cover globals. % \end{itemize} % I'd like to see if better use of Matita's features can help with this stuff. % \bigskip % Open to suggestions for better methods. % } Next, prove that flattening these traces yields the original. } \frame{