Changeset 1845 for Deliverables


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

Minor WP3 revisions prior to more major stuff.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP3.tex

    r1836 r1845  
    11\documentclass[nopanel]{beamer}
     2\usepackage{graphicx,color}
    23
    34\usetheme{Frankfurt}
     
    1920%\SetUnicodeOption{postscript}
    2021%\usepackage{hyperref}
    21 \usepackage{graphicx,color}
    2222\usepackage{latexsym}
    2323\usepackage{listings}
     
    213213
    214214\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'==')
    218217\end{frame}
    219218
     
    238237}
    239238
    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 horrible
    248 % \begin{itemize}
    249 % \item Clight does not permit calls in expressions
    250 % \item Need to add statements in front of the target expression
    251 % \item Messy, duplication
    252 % \item Hard: just noticed that even the prototype gets it wrong
    253 % \end{itemize}
    254 % \item Implemented, but\dots
    255 % \end{itemize}
    256 
    257 % \textsc{Proposal}: shift to later in the compilation process
    258 % \begin{itemize}
    259 % \item easy substitution
    260 % \item adjust semantics to emit extra cost labels
    261 % \item get to use lower level features
    262 % \end{itemize}
    263 % }
    264239\section{Cminor}
    265240\begin{frame}[fragile]
     
    272247\end{itemize}
    273248
    274 % TODO: update!
    275249\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
    276250inductive expr : typ $\rightarrow$ Type[0] ≝
     
    635609
    636610\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 % }
     611Next, prove that flattening these traces yields the original.
     612}
    662613
    663614\frame{
Note: See TracChangeset for help on using the changeset viewer.