Changeset 667 for Deliverables/D1.1/Presentations
 Timestamp:
 Mar 10, 2011, 1:45:46 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.1/Presentations/WP4dominic.tex
r650 r667 14 14 % \usepackage{microtype} 15 15 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} 18 18 \date{March 11, 2011} 19 19 … … 41 41 42 42 \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} 44 Implement an executable semantics of machine code of target processor. 45 \begin{itemize} 46 \item 47 Task 4.1: Executable semantics of machine code (D4.1, month 10). 48 \item 49 Task 4.2: Functional encoding in Calculus of Inductive Constructions (D4.2, month 18). 50 \item 51 Task 4.3: Formal semantics of intermediate languages (D4.3, month 18). 52 \item 53 Task 4.4: Correctness proofs (D4.4, month 36). 54 \end{itemize} 55 Only Task 4.1 was active. Delivered O'Caml and Matita formalisations of MCS51 processor. 56 \end{frame} 57 58 \begin{frame} 59 \frametitle{People involved} 60 \begin{tabular}{lll} 61 Name & Position & Hours \\ 62 \hline 63 Dominic Mulligan & Postdoc & 609 hours \\ 64 Claudio Sacerdoti Coen & Assistant Professor & 16 hours 65 \end{tabular} 49 66 \end{frame} 50 67
Note: See TracChangeset
for help on using the changeset viewer.