source: Deliverables/D1.2/Presentations/WP4-dominic.tex @ 1829

\documentclass[serif]{beamer}

\usepackage[english]{babel}
\usepackage{listings}
\usepackage{microtype}

\usetheme{Frankfurt}
\logo{\includegraphics[height=1.0cm]{fetopen.png}}

\author{Dominic Mulligan}
\title{CerCo Work Package 4}
\date{CerCo project review meeting\\March 2012}

\lstdefinelanguage{matita-ocaml}
  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try},
   morekeywords={[2]whd,normalize,elim,cases,destruct},
   morekeywords={[3]type,of},
   mathescape=true,
  }

\lstset{language=matita-ocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false,
        keywordstyle=\color{red}\bfseries,
        keywordstyle=[2]\color{blue},
        keywordstyle=[3]\color{blue}\bfseries,
        commentstyle=\color{green},
        stringstyle=\color{blue},
        showspaces=false,showstringspaces=false}

\begin{document}

\begin{frame}
\maketitle
\end{frame}

\begin{frame}
\frametitle{Summary I}
Relevant tasks: T4.2 and T4.3 (from the CerCo Contract):
\begin{quotation}
\textbf{Task 4.2}
Functional encoding in the Calculus of Inductive Construction (indicative effort: UNIBO: 8; UDP: 2; UEDIN: 0)
\end{quotation}

\begin{quotation}
\textbf{Task 4.3}
Formal semantics of intermediate languages (indicative effort: UNIBO: 4; UDP: 0; UEDIN: 0)
\end{quotation}
\end{frame}

\begin{frame}
\frametitle{Summary II}
Task 4.2 in detail (from the CerCo Contract):
\begin{quotation}
\textbf{CIC encoding: Back-end}:
Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler.
This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2.
A first validation of the design principles and implementation choices for the Untrusted Cost-annotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Cost-annotating OCaml Compiler sources.
\end{quotation}
\end{frame}

\begin{frame}
\frametitle{Summary III}
Task 4.3 in detail (from the CerCo contract):
\begin{quotation}
\textbf{Executable Formal Semantics of back-end intermediate languages}:
This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it.
\end{quotation}
\end{frame}

\begin{frame}
\frametitle{Backend intermediate languages I}
\begin{itemize}
\item
O'Caml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN
\item
RTLabs is the `frontier' between backend and frontend, last abstract language
\item
RTLabs, RTL, ERTL and LTL are graph based languages: functions represented as graphs of statements, with entry and exit points
\item
LIN is a linearised form of LTL, and is the exit point of the compiler's backend
\item
In contrast to frontend, backend is very different to CompCert's
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Backend intermediate languages II}
\begin{small}
\begin{tabbing}
\quad \=\,\quad \= \\
\textsf{RTLabs}\\
\> $\downarrow$ \> copy propagation (an endo-transformation, yet to be ported) \\
\> $\downarrow$ \> instruction selection\\
\> $\downarrow$ \> change of memory models in compiler\\
\textsf{RTL}\\
\> $\downarrow$ \> constant propagation (an endo-transformation, yet to be ported) \\
\> $\downarrow$ \> calling convention made explicit \\
\> $\downarrow$ \> layout of activation records \\
\textsf{ERTL}\\
\> $\downarrow$ \> register allocation and spilling\\
\> $\downarrow$ \> dead code elimination\\
\textsf{LTL}\\
\> $\downarrow$ \> function linearisation\\
\> $\downarrow$ \> branch compression (an endo-transformation) \\
\textsf{LIN}\\
\> $\downarrow$ \> relabeling\\
\end{tabbing}
\end{small}
\end{frame}

\begin{frame}
\frametitle{\texttt{Joint}: a new approach I}
\begin{itemize}
\item
Consecutive languages in backend must be similar
\item
Transformations between languages translate away some small specific set of features
\item
But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated
\item
Not clear if translation passes can commute, for instance
\item
CerCo passes are in a different order to CompCert (calling convention and register allocation done in different places)
\item
Instruction selection done early: changing subset of instructions used would require instructions to be duplicated everywhere in backend
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{\texttt{Joint}: a new approach II}
\begin{itemize}
\item
Idea: all of these languages are just instances of a single language
\item
This language \texttt{Joint} is parameterised by a type of registers to be used in instructions, and so forth
\item
Each language after RTLabs is now just defined as the \texttt{Joint} language instantiated with some concrete types
\item
Similarly for semantics: common definitions that take e.g. type representing program counters as parameters
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{\texttt{Joint}: a new approach III}
\texttt{Joint} instructions allow us to embed language-specific instructions:
\begin{lstlisting}
inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
 | COMMENT: String $\rightarrow$ joint_instruction p globals
 | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
 ...
 | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals
 | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
\end{lstlisting}

\begin{lstlisting}
inductive ertl_statement_extension: Type[0] :=
 | ertl_st_ext_new_frame: ertl_statement_extension
 | ertl_st_ext_del_frame: ertl_statement_extension
 | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension.
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{\texttt{Joint}: a new approach IV}
For example, the definition of the \texttt{ERTL} language is now:
\begin{lstlisting}
inductive move_registers: Type[0] :=
 | pseudo: register $\rightarrow$ move_registers
 | hardware: Register $\rightarrow$ move_registers.

definition ertl_params__: params__ :=
 mk_params__ register register register register
  (move_registers $\times$ move_registers)
   register nat unit ertl_statement_extension.
definition ertl_params_: params_ :=
 graph_params_ ertl_params__.
definition ertl_params0: params0 :=
 mk_params0 ertl_params__ (list register) nat.
definition ertl_params1: params1 :=
 rtl_ertl_params1 ertl_params0.
definition ertl_params: $\forall$globals. params globals ≝
 rtl_ertl_params ertl_params0.
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Instruction embedding in \texttt{Joint}}
\begin{lstlisting}
inductive joint_instruction (p:params__) (globals: list ident): Type[0] :=
 ...
 | POP: acc_a_reg p $\rightarrow$ joint_instruction p globals
 | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals
 ...
\end{lstlisting}
\begin{itemize}
\item
RTLabs (not a \texttt{Joint} language) to RTL is where instruction selection takes place
\item
Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{\texttt{Joint}: advantages}
\begin{itemize}
\item
Why use \texttt{Joint}, as opposed to defining all languages individually?
\item
Reduces repeated code (fewer bugs, or places to change)
\item
Unify some proofs, making correctness proof easier
\item
Easier to add new intermediate languages as needed
\item
Easier to see relationship between consecutive languages at a glance
\item
Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted)
\item
We can investigate which translation passes commute much more easily
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Semantics of \texttt{Joint} I}
\begin{itemize}
\item
As mentioned, use of \texttt{Joint} also unifies semantics of these languages
\item
We use several sets of records, which represent the state that a program is in
\item
These records are parametric in representations for e.g. frames
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Semantics of \texttt{Joint} II}
\begin{lstlisting}
record more_sem_params (p:params_): Type[1] :=
{
  framesT: Type[0];
  empty_framesT: framesT;
  regsT: Type[0];
  ...
  acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
  acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval;
  ...
  pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT
 }.
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Semantics of \texttt{Joint} III}
Generic functions:
\begin{lstlisting}
definition set_carry: $\forall$p. beval $\rightarrow$ state p $\rightarrow$ state p :=
 $\lambda$p, carry, st.
  mk_state $\ldots$ (st_frms $\ldots$ st) (pc $\ldots$ st)
   (sp $\ldots$ st) (isp $\ldots$ st) carry (regs $\ldots$ st) (m $\ldots$ st).
\end{lstlisting}
\begin{lstlisting}
definition goto: $\forall$globals. $\forall$p:sem_params1 globals. genv globals p $\rightarrow$
  label $\rightarrow$ state p $\rightarrow$ res (state p) :=
 $\lambda$globals, p, ge, l, st.
  do oldpc $\leftarrow$ pointer_of_address (pc $\ldots$ st) ;
  do newpc $\leftarrow$ address_of_label $\ldots$ ge oldpc l ;
  OK $\ldots$ (set_pc $\ldots$ newpc st).
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Semantics of \texttt{Joint} IV}
Individual semantics obtained by instantiating records to concrete types (ERTL here):
\begin{lstlisting}
definition ertl_more_sem_params: more_sem_params ertl_params_ :=
 mk_more_sem_params ertl_params_
  (list (register_env beval)) [] ((register_env beval) $\times$ hw_register_env)
   ($\lambda$sp. $\langle$empty_map $\ldots$,init_hw_register_env sp$\rangle$) 0 it
   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store
    ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     ($\lambda$locals,dest_src.
       do v $\leftarrow$
        match \snd dest_src with
        [ pseudo reg $\Rightarrow$ ps_reg_retrieve locals reg
        | hardware reg $\Rightarrow$ hw_reg_retrieve locals reg
        ];
       match \fst dest_src with
       [ pseudo reg $\Rightarrow$ ps_reg_store reg v locals
       | hardware reg $\Rightarrow$ hw_reg_store reg v locals
       ]).
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Semantics of \texttt{Joint} V}
For languages with `extensions', we provide a semantics:
\begin{lstlisting}
definition ertl_exec_extended:
 $\forall$globals. genv globals (ertl_params globals) $\rightarrow$
  ertl_statement_extension $\rightarrow$ label $\rightarrow$ state ertl_sem_params $\rightarrow$
   IO io_out io_in (trace $\times$ (state ertl_sem_params)) :=
 $\lambda$globals, ge, stm, l, st.
  match stm with
   [ ertl_st_ext_new_frame $\Rightarrow$
      ! v $\leftarrow$ framesize globals $\ldots$ ge st;
      let sp := get_hwsp st in
      ! newsp $\leftarrow$ addr_sub sp v;
      let st := set_hwsp newsp st in
      ! st $\leftarrow$ next $\ldots$ (ertl_sem_params1 globals) l st ;
        ret ? $\langle$E0, st$\rangle$
   | ...
   ].
\end{lstlisting}
\end{frame}

\begin{frame}
\frametitle{\texttt{Joint} summary}
\begin{itemize}
\item
Using \texttt{Joint} we get a modular semantics
\item
`Common' semantics are shared amongst all languages
\item
Specific languages are responsible for providing the semantics of the extensions that they provide
\item
Show differences (and similarities) between languages clearly
\item
Reduces proofs
\item
Easy to add new languages
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{A new intermediate language}
\begin{itemize}
\item
Matita backend includes a new intermediate language: RTLntc
\item
Sits between RTL and ERTL
\item
RTLntc is the RTL language where all tailcalls have been eliminated
\item
This language is `implicit' in the O'Caml compiler
\item
There, the RTL to ERTL transformation eliminates tailcalls as part of translation
\item
But including an extra, explicit intermediate language is `almost free' using the \texttt{Joint} language approach
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{The LTL to LIN transform I}
\begin{itemize}
\item
\texttt{Joint} clearly separates fetching from program execution
\item
We can vary how one works whilst fixing the other
\item
Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation
\item
The order of transformations in O'Caml prototype is fixed
\item
Linearisation takes place at a fixed place, in the translation between LTL and LIN
\item
The Matita compiler is different: linearisation is a generic process
\item
Any graph-based language can now be linearised
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{The LTL to LIN transform II}
\begin{itemize}
\item
The CompCert backend linearises much sooner than CerCo's
\item
We can now experiment with linearising much earlier
\item
Many transformations and optimisations can work fine on a linearised form
\item
The only place in the backend that requires a graph-based language is in the ERTL pass, where we do a dataflow analysis
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{`Free time'}
\begin{itemize}
\item
We had six months of time which is not reported on in any deliverable
\item
We invested this time working on:
\begin{itemize}
\item
The global proof sketch
\item
The setup of `proof infrastructure', common definitions, lemmas, invariants etc. required for main body of proof
\item
The proof of correctness for the assembler
\item
A notion of `structured traces', used throughout the compiler formalisation, as a means of eventually proving that the compiler correctly preserves costs
\item
Structured traces were defined in collaboration with the team at UEDIN
\end{itemize}
\item
I now explain in more detail how this time was used
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Assembler}
\begin{itemize}
\item
After LIN, compiler spits out assembly language for MCS-51
\item
Assembler has pseudoinstructions similar to many commercial assembly languages
\item
For instance, instead of computed jumps (e.g. \texttt{SJMP} to a specific address), compiler can simply spit out a generic jump instruction to a label
\item
Simplifies the compiler, at the expense of introducing more proof obligations
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{A problem: jump expansion}
\begin{itemize}
\item
`Jump expansion' is our name for the standard `branch displacement' problem
\item
Given a pseudojump to a label $l$, how best can this be expanded into an assembly instruction \texttt{SJMP}, \texttt{AJMP} or \texttt{LJMP} to a concrete address?
\item
Problem also applies to conditional jumps
\item
Problem especially relevant for MCS-51 as it has a small code memory, therefore aggressive expansion of jumps into smallest possible concrete jump instruction needed
\item
But a known hard problem (NP-complete depending on architecture), and easy to imagine knotty configurations where size of jumps are interdependent
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Jump expansion I}
\begin{itemize}
\item
We employed the following tactic: split the decision over how any particular pseudoinstruction is expanded from pseudoinstruction expansion
\item
Call the decision maker a `policy'
\item
We started the proof of correctness for the assembler based on the premise that a correct policy exists
\item
Further, we know that the assembler only fails to assemble a program if a good policy does not exist (a side-effect of using dependent types)
\item
A bad policy is a function that expands a given pseudojump into a concrete jump instruction that is `too small' for the distance to be jumped, or makes the program consume too much memory
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Jump expansion II}
\begin{itemize}
\item
Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51
\item
The strategy initially translates all pseudojumps as \texttt{SJMP} and then increases their size if necessary
\item
Termination of the procedure is proved, as well as a safety property, stating that jumps are not expanded into jumps that are too long
\item
His strategy is not optimal (though the computed solution is optimal for the strategy employed)
\item
Boender's work is the first formal treatment of the `jump expansion problem'
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Assembler correctness proof}
\begin{itemize}
\item
Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler
\item
Boender's work has just been completed (modulo a few missing lemmas)
\item
We abandoned the main assembler proof to start work on other tasks (and wait for Boender to finish)
\item
However, we intend to return to the proof, and publishing an account of the work (possibly) as a journal paper
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Who pays? I}
\begin{lstlisting}
int main(int argc, char** argv) {
  label1:
    ...
    some_function();
  label2:
    ...
}
\end{lstlisting}
\begin{itemize}
\item
Question: where do we put cost labels to capture execution costs?
\item
Proof obligations complicated by panoply of labels
\item
Doesn't work well with \texttt{g(h() + 2 + f())}
\item
To prove accuracy we need to show \texttt{some\_function()} terminates!
\item
\texttt{some\_function()} may not return correctly
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Who pays? II}
\begin{itemize}
\item
Solution: omit \texttt{label2} and just keep \texttt{label1}
\item
We pay for everything `up front' when entering a function
\item
No need to prove \texttt{some\_function()} terminates
\item
But now execution of functions in CerCo takes a particular form
\item
Functions begin with a label, call other functions that begin with a label, eventually return, but \emph{return} to the correct place
\item
`Recursive structure'
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Structured traces I}
\begin{itemize}
\item
We introduced a notion of `structured traces'
\item
These are intended to statically capture the (good) execution traces of a program
\item
That is, functions return to where they ought
\item
Come in two variants: inductive and coinductive
\item
Inductive is meant to capture program execution traces that eventually halt
\item
Coinductive is meant to capture program execution traces that diverge
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Structured traces II}
\begin{itemize}
\item
Here, I focus on the inductive variety
\item
Used the most (for now) in the backend
\item
In particular, used in the proof that static and dynamic cost computations coincide
\item
This will be explained later
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Structured traces III}
\begin{itemize}
\item
Central insight is that program execution is always in the body of some function (from \texttt{main} onwards)
\item
A well formed program must have labels appearing at certain spots
\item
Similarly, the final instruction executed when executing a function must be a \texttt{RET}
\item
Execution must then continue in body of calling function, at correct place
\item
These invariants, and others, are crystalised in the specific syntactic form of a structured trace
\item
Some examples...
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Structured trace examples I}
Traces end with a return being executed, or not:
\begin{lstlisting}
inductive trace_ends_with_ret: Type[0] :=
 | ends_with_ret: trace_ends_with_ret
 | doesnt_end_with_ret: trace_ends_with_ret.
\end{lstlisting}
A trace starting with a label and ending with a return:
\begin{lstlisting}
inductive trace_label_return (S: abstract_status): S $\rightarrow$ S $\rightarrow$ Type[0] :=
 | tlr_base:
  $\forall$status_before: S.
  $\forall$status_after: S.
   trace_label_label S ends_with_ret status_before status_after $\rightarrow$
    trace_label_return S status_before status_after
  ...
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Structured trace examples II}
A trace starting and ending with a cost label:
\begin{lstlisting}
...
with trace_label_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
 | tll_base:
  $\forall$ends_flag: trace_ends_with_ret.
  $\forall$start_status: S.
  $\forall$end_status: S.
   trace_any_label S ends_flag start_status end_status $\rightarrow$
   as_costed S start_status $\rightarrow$
    trace_label_label S ends_flag start_status end_status
...
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Structured trace examples III}
A call followed by a label on return:
\begin{lstlisting}
...
with trace_any_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
...
 | tal_base_call:
  $\forall$status_pre_fun_call: S.    
  $\forall$status_start_fun_call: S.
  $\forall$status_final: S.
   as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
   $\forall$H:as_classifier S status_pre_fun_call cl_call.
    as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final $\rightarrow$
    trace_label_return S status_start_fun_call status_final $\rightarrow$
    as_costed S status_final $\rightarrow$
     trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
...
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Structured trace examples IV}
A call followed by a non-empty trace:
\begin{lstlisting}
...
| tal_step_call:
 $\forall$end_flag: trace_ends_with_ret.
 $\forall$status_pre_fun_call: S.
 $\forall$status_start_fun_call: S.
 $\forall$status_after_fun_call: S.
 $\forall$status_final: S.
  as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
  $\forall$H:as_classifier S status_pre_fun_call cl_call.
   as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call $\rightarrow$
   trace_label_return S status_start_fun_call status_after_fun_call $\rightarrow$
   ¬ as_costed S status_after_fun_call $\rightarrow$
   trace_any_label S end_flag status_after_fun_call status_final $\rightarrow$
    trace_any_label S end_flag status_pre_fun_call status_final
...
\end{lstlisting}
\end{frame}

\begin{frame}
\frametitle{Static and dynamic costs I}
\begin{itemize}
\item
Given a structured trace, we can compute its associated cost
\item
This is the \emph{static} cost of a program execution
\item
Similarly, given a program counter and a code memory (corresponding to the trace), we can compute a \emph{dynamic cost} of a simple block
\item
Do this by repeatedly fetching, obtaining the next instruction, and a new program counter
\item
This requires some predicates defining what a `good program' and what a `good program counter' are
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Static and dynamic costs II}
\begin{itemize}
\item
We aim to prove that the dynamic and static cost calculations coincide
\item
This would imply that the static cost computation is correct
\item
This proof is surprisingly tricky to complete (about 3 man months of work so far)
\item
Is now about 95\% complete
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Changes ported to O'Caml prototype}
\begin{itemize}
\item
Bug fixes spotted in the formalisation so far have been merged back into the O'Caml compiler
\item
Larger changes like the \texttt{Joint} machinery have so far not
\item
It is unclear whether they will be
\item
Just a generalisation of what is already there
\item
Supposed to make formalisation easier
\item
Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C
\item
Porting a large change to the untrusted compiler would jeopardise these experiments
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Improvements in Matita}
\begin{itemize}
\item
Part of the motivation for using Matita was for CerCo to act a `stress test'
\item
The proofs talked about in this talk have done this
\item
Many improvements to Matita have been made since the last project meeting
\item
These include major speed-ups of e.g. printing large goals, bug fixes, the porting of CerCo code to standard library, and more options for passing to tactics
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{The next period}
UNIBO has following pool of remaining manpower (postdocs):
\begin{center}
\begin{tabular}{ll}
Person & Man months remaining \\
\hline
Boender & 14 months \\
Mulligan & 6 months \\
Tranquilli & 10 months \\
\end{tabular}
\end{center}
\begin{itemize}
\item
Boender finishing assembler correctness proof
\item
Mulligan proofs of correctness for 1 intermediate language
\item
Tranquilli proofs of correctness for 2 intermediate languages
\item
Sacerdoti Coen `floating'
\item
Believe we have enough manpower to complete backend
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Summary}
We have:
\begin{itemize}
\item
Translated the O'Caml prototype's backend intermediate languages into Matita
\item
Implemented the translations between languages, and given the intermediate languages a semantics
\item
Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised
\item
Spotted opportunities for possibly commuting backend translation passes
\item
Used six months to define structured traces and start the proof of correctness for the assembler
\item
Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler
\end{itemize}
\end{frame}

\end{document}