Changeset 1845 for Deliverables/D1.2

Timestamp:

Mar 15, 2012, 2:14:54 PM (9 years ago)

Author:

campbell

Message:

Minor WP3 revisions prior to more major stuff.

File:

• Deliverables/D1.2/Presentations/WP3.tex (modified) (6 diffs)

Deliverables/D1.2/Presentations/WP3.tex

@@ -1 +1 @@
 \documentclass[nopanel]{beamer}
+\usepackage{graphicx,color}
 
 \usetheme{Frankfurt}
@@ -19 +20 @@
 %\SetUnicodeOption{postscript}
 %\usepackage{hyperref}
-\usepackage{graphicx,color}
 \usepackage{latexsym}
 \usepackage{listings}
@@ -213 +213 @@
 
 \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}
 
@@ -238 +237 @@
 }
 
-% \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]
@@ -272 +247 @@
 \end{itemize}
 
-% TODO: update!
 \begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
 inductive expr : typ $\rightarrow$ Type[0] ≝
@@ -635 +609 @@
 
 \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{