Changeset 620 for Deliverables/D1.1


Ignore:
Timestamp:
Mar 2, 2011, 3:56:18 PM (9 years ago)
Author:
mulligan
Message:

More changes to presentation. Modified some of the C examples to test for Ayache's reported bug.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.1/Presentations/WP4-dominic-presentation.tex

    r618 r620  
    44\logo{\includegraphics[height=1.0cm]{fetopen.png}}
    55
     6\usepackage{amsfonts}
     7\usepackage{amsmath}
     8\usepackage{amssymb}
    69\usepackage[english]{babel}
    7 \usepackage{inputenc}
     10\usepackage{color}
     11\usepackage[utf8x]{inputenc}
     12\usepackage{listings}
     13\usepackage{stmaryrd}
     14% \usepackage{microtype}
    815
    916\author{Dominic P. Mulligan and Claudio Sacerdoti Coen}
     
    1320\setlength{\parskip}{1em}
    1421
     22\lstdefinelanguage{matita-ocaml}
     23  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
     24   morekeywords={[2]whd,normalize,elim,cases,destruct},
     25   morekeywords={[3]type,of,val,assert,let,function},
     26   mathescape=true,
     27  }
     28\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
     29        keywordstyle=\color{red}\bfseries,
     30        keywordstyle=[2]\color{blue},
     31        keywordstyle=[3]\color{blue}\bfseries,
     32        commentstyle=\color{green},
     33        stringstyle=\color{blue},
     34        showspaces=false,showstringspaces=false}
     35
    1536\begin{document}
    1637
     
    105126\end{frame}
    106127
    107 \begin{frame}
     128\begin{frame}[fragile]
    108129\frametitle{Polymorphic variants and phantom types}
    109 \begin{itemize}
    110 \item
    111130The instruction set is highly non-orthogonal.
    112 \item
    113 We needed a way of
    114 \end{itemize}
    115 \end{frame}
    116 
    117 \begin{frame}
    118 \frametitle{Use of dependent types}
     131We used polymorphic variants and phantom types to capture this non-orthogonality in the type system.
     132For instance:
     133
     134\begin{small}
     135\begin{lstlisting}
     136type direct = [ `DIRECT of byte ]
     137type indirect = [ `INDIRECT of bit ]
     138...
     139type 'addr preinstruction =
     140 [ `ADD of acc * [ reg | direct | indirect | data ]
     141...
     142 | `MOV of
     143    (acc * [ reg | direct | indirect | data ],
     144     [ reg | indirect ] * [ acc | direct | data ],
     145     direct * [ acc | reg | direct | indirect | data ], ...)
     146...
     147\end{lstlisting}
     148\end{small}
     149\end{frame}
     150
     151\begin{frame}[fragile]
     152\frametitle{Use of dependent types I}
     153This approach worked well in O'Caml, but Matita does not have polymorphic variants, so we need a substitute.
     154We use dependent types.
     155
     156Introduce a type for addressing modes:
     157\begin{small}
     158\begin{lstlisting}
     159inductive addressing_mode: Type[0] :=
     160  DIRECT: Byte $\rightarrow$ addressing_mode
     161...
     162\end{lstlisting}
     163\end{small}
     164And another type \texttt{addressing\_mode\_tag} of `tags' whose constructors are in correspondence with those of \texttt{addressing\_mode}.
     165\end{frame}
     166
     167\begin{frame}[fragile]
     168\frametitle{Use of dependent types II}
     169We use vectors of \texttt{addressing\_mode\_tag}s in our type signatures for instructions.
     170For instance:
     171\begin{small}
     172\begin{lstlisting}
     173inductive preinstruction (A: Type[0]): Type[0] :=
     174   ADD: $\llbracket$ acc_a $\rrbracket$
     175        $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$
     176        $\rightarrow$ preinstruction A
     177...
     178\end{lstlisting}
     179\end{small}
     180We need: an \emph{ad hoc} $\Sigma$ type and two coercions.
     181One coercion automatically opens up a proof obligation when it is used, which requires some lemmas.
     182
     183These lemmas and automation close all proof obligations generated (over 300 in typechecking the main interpreter function).
     184\end{frame}
     185
     186\begin{frame}
     187\frametitle{Overlapping memory spaces and addressing modes}
     188MCS-51 memory spaces overlap, and can be addressed using different modes and sized pointers.
     189The status record models memory merely as disjoint spaces, using a `tries with holes' datastructure.
     190
     191All complications to do with overlapping are handled
    119192\end{frame}
    120193
Note: See TracChangeset for help on using the changeset viewer.