source: Deliverables/D1.1/Presentations/WP6-claudio.tex @ 3534

\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 11, 2011}

\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] \alert{Project Web Site and Software Repository}
 \item[D6.2] \alert{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, D6.1 and D6.2 were due in the first period.
\end{frame}

\begin{frame}
 \frametitle{D6.1: Project Web site and Software Repository}
 Goals:
  \begin{itemize}
   \item Services to the project members
     \begin{enumerate}
      \item to allow a timely and effective \alert{communication} between partners
      \item to allow \alert{collaborative work} on the software and reports produced
      \item to keep an \alert{historical trace} of the decision taken and of the
        evolution of the deliverables
     \end{enumerate}
   \item Services to the public
     \begin{enumerate}
      \item to advertise the project, its aims and its results to a wide
        audience
      \item to help dissemination and allow downloading of the deliverables
      \item to \alert{gather feedback from the users}
     \end{enumerate}
  \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{D6.1: Project Web site and Software Repository}
 Setup:
 \begin{itemize}
  \item a \alert{private mailing list} for developers
  \item a \alert{Wiki}-based public Web site
  \item a \alert{private part} of the Wiki for developers only
  \item an integrated \alert{issue tracking} system
  \item a Subversion (SVN) \alert{software repository}
  \item a continuous building system for the version of Matita in use
        in the project
 \end{itemize}
\end{frame}

\begin{frame}
 \includegraphics[height=9.0cm]{figs/website.pdf}
\end{frame}

%\begin{frame}
% \frametitle{D6.2: Plan for the Use and dissemination of foreground}
%\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 List of presentations given to \alert{international conferences}:

 \begin{itemize}
  \item \alert{Certified Complexity}, talk given by Claudio Sacerdoti Coen at Types
    2010, Warsaw (15 October 2010)
  \item \alert{Realisability Models for Cost-Preserving Compiler Correctness}, talk to
    be 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)
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 List of presentations given to \alert{inviting institutions}:
 \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 r^2$ (26 November 2010)
  \item \alert{Certifying cost annotations in compilers}, talk given by Roberto Amadio at ENS/Lyon.
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 \alert{Other seminars:}
 \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)
 \end{itemize}
\end{frame}

\begin{frame}
 \frametitle{Dissemination activity}
 Papers \alert{currently submitted:}
 \begin{itemize}
  \item \alert{An executable formalisation of the MCS-51 microprocessor in Matita}, Dominic Mulligan and Claudio Sacerdoti Coen. Submitted to Interactive Theorem Proving 2011
  \item \alert{Certified complexity}, Dominic Mulligan and Claudio Sacerdoti Coen. Poster submission at FET11
  \item \alert{The Matita Interactive Theorem Prover}, Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico Tassi. System description submitted to CADE 2011
  \item \alert{Certifying cost annotations in compilers}, Roberto Amadio, Nicolas Ayache, Yann Regis-Gianas, Ronan Saillard. Submitted to Formal Methods 2011
  \item \alert{Elementary affine lambda-calculus with multithreading and side effects}, A. Madet, R. Amadio. Submitted to TLCA 2011
  \item \alert{A decompilation of the pi-calculus and its applications to termination}, Roberto Amadio. Submitted to ICALP 2011.
 \end{itemize}
\end{frame}

\end{document}