source: Deliverables/D1.2/Presentations/WP6-claudio.tex @ 2097

\documentclass{beamer}

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

\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[english]{babel}
\usepackage{color}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{stmaryrd}
\usepackage{fancyvrb}
% \usepackage{microtype}

\author{Claudio Sacerdoti Coen}
\title{Certified Complexity (CerCo)\\
       Dissemination activities and future work}
\date{March 16, 2012}

\setlength{\parskip}{1em}

\AtBeginSection[]
{
  \begin{frame}<beamer>
    \frametitle{Outline}
    \tableofcontents[currentsection]
  \end{frame}
}

\begin{document}

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

%\begin{frame}
  %\frametitle{Outline}
  %\tableofcontents
%\end{frame}

\section{Dissemination activities}

\begin{frame}
 \frametitle{Objectives of WP6}
\begin{center}
 ``To \alert{manage the knowledge} generated by the project and IPRs, and to bring the \alert{technological advances} developed within the CerCo project to the \alert{scientific community} and \alert{potential users}''
\end{center}

Specific objectives:
 \begin{itemize}
  \item a tailored \alert{dissemination activity} that will make use of specific
    dissemination mechanisms in order to reach the relevant communities
  \item supervision of the entire project with regard to \alert{result applicability} and the promotion of the exploitation
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Structure of WP6}
{\small
\begin{description}
 \item[Task 6.1] User validation and exploitability
 \item[Task 6.2] \alert{Contribution to portfolio and concertation activities at FET-Open level}
 \item[D6.1] Project Web Site and Software Repository
 \item[D6.2] Plan for the Use and dissemination of foreground
 \item[D6.3] Final report on user validation
 \item[D6.4] Organisation of an Event Targeted to Potential Industrial Stakeholders
 \item[D6.5] Organisation of an Event Targeted to Potential Industrial Stakeholders
 \item[D6.6] Packages for Linux distributions and Live CD
\end{description}}
Only T6.2 was due in the second period.
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 \alert{Papers} published:
\small
\begin{itemize}
        \item \alert{A Canonical Locally Named Representation of Binding}, R. Pollack,
        M. Sato and W.  Ricciotti, Journal of Automated Reasoning
        \item \alert{Certifying and reasoning on cost annotations of functional
        programs}, R.M. Amadio, Y.Regis-Gianas, Proceedings of FOPARA 2011
        \item \alert{An Elementary Affine $\lambda$-Calculus with Multithreading and
        Side Effects}, A. Madet, R.M. Amadio, Proceedings of TLCA 2011
        \item \alert{Certified Complexity}, R. Armadio, A. Asperti, N. Ayache, B.
        Campbell, D. Mulligan, R.  Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
        Stark, in Proceedings of FET 11
        \item \alert{The Matita Interactive Theorem Prover}, A.Asperti, W.Ricciotti,
        C. Sacerdoti Coen, E.Tassi, In Automated Deduction – CADE-23, Lecture Notes
        in Computer Science
\end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 Presentations given to \alert{international conferences}:

        \small
\begin{itemize}
        \item \alert{Certified Complexity}, talk given by Claudio Sacerdoti Coen at
        Types 2010, Warsaw (15 October 2010). 
        \item \alert{Realizability Models for Cost-Preserving Compiler Correctness},
        talk given by Marco Gaboardi at DICE 2010. 
        \item \alert{A canonical locally nameless formalisation of an algebraic
        logical framework}, talk given by Wilmer Ricciotti at Types 2010, Warsaw (13
        October 2010). 
        \item \alert{An Elementary Affine $\lambda$-Calculus with Multithreading and
        Side Effects}, talk given by A.  Madet at TLCA 2011 (2 June 2011) 
        \item \alert{A type system for positivity}, talk given by Claudio Sacerdoti
        Coen at Types 2011 (10 September 2011) 
        \item \alert{The Matita Interactive Theorem Prover}, talk given by Wilmer
        Ricciotti at CADE 2011 (3 August 2011) 
\end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
        Posters presented at \alert{international conferences}:

        \small
        \begin{itemize}
                \item \alert{Certified Complexity}. Poster presented by Claudio Sacerdoti
                Coen and Dominic Mulligan at FET 2011, Budapest (4--6 May 2011).
        \end{itemize}
\end{frame}
 
\begin{frame}
 \frametitle{Dissemination activity}
 Presentations given to \alert{inviting institutions}:
\small
\begin{itemize}
        \item \alert{Certifying cost annotations in compilers}, talk given by Nicolas
        Ayache at the LIP6 laboratory of the University Paris 6 (18 November 2010); 
        \item \alert{A canonically nameless representation of binders}, talk given by
        Randy Pollack at U.  Penn at Philadelphia (11 June 2010); 
        \item \alert{A canonically nameless representations of binders}, talk given by
        Randy Pollack at Lab PPS (Paris) to the INRIA-Rocquencourt team $\pi$ r2 
        26 November 2010); 
        \item \alert{Certifying cost annotations in compilers}, talk given by Roberto
        Amadio at ENS/Lyon. 
        \item \alert{Certified Complexity}, talk given by Claudio Sacerdoti Coen at
        the University of Birmingham (20 December 2011). 
        \item \alert{Certifying cost annotations in compilers}, talk given by Nicolas
        Ayache at ENSTA (13 December 2011); 
\end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 \alert{Other seminars:}
        \small
\begin{itemize}
        \item \alert{Operational Semantics in Specifications}, talk given by Brian
        Campbell at the Laboratory for Foundations of Computer Science, University of
        Edinburgh (16 March 2010) 
        \item \alert{An executable semantics for CompCert C}, talk given by Brian
        Campbell at the Scottish Programming Language seminar at Heriot-Watt
        University (11 November 2011). 
\end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 Papers \alert{submitted/to be submitted:}
\small
\begin{itemize}
        \item \alert{An executable semantics for CompCert C}, Brian Campbell.
        \item \alert{A compact proof of decidability for regular expression equivalence}, A. Asperti. Submitted to ITP.
        \item \alert{An executable formalisation of the MCS-51 microprocessor in
        Matita}, Dominic Mulligan and Claudio Sacerdoti Coen. 
        To be integrated in journal paper.
        \item \alert{On the correctness of an assembler for the Intel MCS-51
        microprocessor}, Dominic Mulligan and Claudio Sacerdoti Coen. 
        To be submitted when the proof is completed.
        \item \alert{Certifying cost annotations in compilers}, Roberto Amadio,
        Nicolas Ayache, Yann Regis-Gianas, Ronan Saillard. Submitted to
        FMICS.
\end{itemize}
\end{frame}

\end{document}