Changeset 667


Ignore:
Timestamp:
Mar 10, 2011, 1:45:46 PM (9 years ago)
Author:
mulligan
Message:

Changes to presentation that claudio wanted

File:
1 edited

Legend:

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

    r650 r667  
    1414% \usepackage{microtype}
    1515
    16 \author{Dominic P. Mulligan and Claudio Sacerdoti Coen}
    17 \title{CerCo Work Package 4.1}
     16\author{Dominic P. Mulligan}
     17\title{CerCo Work Package 4}
    1818\date{March 11, 2011}
    1919
     
    4141
    4242\begin{frame}
    43 \frametitle{Work Package 4.1}
    44 Work Package 4.1 entitled `Executable Formal Semantics of Machine Code':
    45 \begin{quote}
    46 Formal definition of the semantics of the target language. The semantics will be given in a functional (and hence executable) form, useful for testing, validation and project assessment.
    47 \end{quote}
    48 Manpower: Dominic Mulligan (609 hours) and Claudio Sacerdoti Coen (16 hours).
     43\frametitle{Work package}
     44Implement an executable semantics of machine code of target processor.
     45\begin{itemize}
     46\item
     47Task 4.1: Executable semantics of machine code (D4.1, month 10).
     48\item
     49Task 4.2: Functional encoding in Calculus of Inductive Constructions (D4.2, month 18).
     50\item
     51Task 4.3: Formal semantics of intermediate languages (D4.3, month 18).
     52\item
     53Task 4.4: Correctness proofs (D4.4, month 36).
     54\end{itemize}
     55Only Task 4.1 was active.  Delivered O'Caml and Matita formalisations of MCS-51 processor.
     56\end{frame}
     57
     58\begin{frame}
     59\frametitle{People involved}
     60\begin{tabular}{lll}
     61Name & Position & Hours \\
     62\hline
     63Dominic Mulligan & Postdoc & 609 hours \\
     64Claudio Sacerdoti Coen & Assistant Professor & 16 hours
     65\end{tabular}
    4966\end{frame}
    5067
Note: See TracChangeset for help on using the changeset viewer.