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

Last change on this file since 676 was 676, checked in by sacerdot, 9 years ago

...

File size: 6.1 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb}
9\usepackage[english]{babel}
10\usepackage{color}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14\usepackage{fancyvrb}
15% \usepackage{microtype}
16
17\author{Claudio Sacerdoti Coen}
18\title{Certified Complexity (CerCo)\\
19       Dissemination activities and future work}
20\date{March 11, 2011}
21
22\setlength{\parskip}{1em}
23
24\AtBeginSection[]
25{
26  \begin{frame}<beamer>
27    \frametitle{Outline}
28    \tableofcontents[currentsection]
29  \end{frame}
30}
31
32\begin{document}
33
34\begin{frame}
35\maketitle
36\end{frame}
37
38\begin{frame}
39  \frametitle{Outline}
40  \tableofcontents
41\end{frame}
42
43\section{Dissemination activities}
44
45\begin{frame}
46 \frametitle{Objectives of WP6}
47\begin{center}
48 ``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}''
49\end{center}
50
51Specific objectives:
52 \begin{itemize}
53  \item a tailored \alert{dissemination activity} that will make use of specific
54    dissemination mechanisms in order to reach the relevant communities
55  \item supervision of the entire project with regard to \alert{result applicability} and the promotion of the exploitation
56 \end{itemize}
57\end{frame}
58
59\begin{frame}
60 \frametitle{Structure of WP6}
61{\small
62\begin{description}
63 \item[Task 6.1] User validation and exploitability
64 \item[Task 6.2] \alert{Contribution to portfolio and concertation activities at FET-Open level}
65 \item[D6.1] \alert{Project Web Site and Software Repository}
66 \item[D6.2] \alert{Plan for the Use and dissemination of foreground}
67 \item[D6.3] Final report on user validation
68 \item[D6.4] Organisation of an Event Targeted to Potential Industrial Stakeholders
69 \item[D6.5] Organisation of an Event Targeted to Potential Industrial Stakeholders
70 \item[D6.6] Packages for Linux distributions and Live CD
71\end{description}}
72Only T6.2, D6.1 and D6.2 were due in the first period.
73\end{frame}
74
75\begin{frame}
76 \frametitle{D6.1: Project Web site and Software Repository}
77 Goals:
78  \begin{itemize}
79   \item Services to the project members
80     \begin{enumerate}
81      \item to allow a timely and effective \alert{communication} between partners
82      \item to allow \alert{collaborative work} on the software and reports produced
83      \item to keep an \alert{historical trace} of the decision taken and of the
84        evolution of the deliverables
85     \end{enumerate}
86   \item Services to the public
87     \begin{enumerate}
88      \item to advertise the project, its aims and its results to a wide
89        audience
90      \item to help dissemination and allow downloading of the deliverables
91      \item to \alert{gather feedback from the users}
92     \end{enumerate}
93  \end{itemize}
94\end{frame}
95
96\begin{frame}
97 \frametitle{D6.1: Project Web site and Software Repository}
98 Setup:
99 \begin{itemize}
100  \item a \alert{private mailing list} for developers
101  \item a \alert{Wiki}-based public Web site
102  \item a \alert{private part} of the Wiki for developers only
103  \item an integrated \alert{issue tracking} system
104  \item a Subversion (SVN) \alert{software repository}
105  \item a continuous building system for the version of Matita in use
106        in the project
107 \end{itemize}
108\end{frame}
109
110\begin{frame}
111 \includegraphics[height=9.0cm]{figs/website.pdf}
112\end{frame}
113
114%\begin{frame}
115% \frametitle{D6.2: Plan for the Use and dissemination of foreground}
116%\end{frame}
117
118\begin{frame}
119 \frametitle{Dissemination activity}
120 List of presentations given to \alert{international conferences}:
121
122 \begin{itemize}
123  \item \alert{Certified Complexity}, talk given by Claudio Sacerdoti Coen at Types
124    2010, Warsaw (15 October 2010)
125  \item \alert{Realisability Models for Cost-Preserving Compiler Correctness}, talk to
126    be given by Marco Gaboardi at DICE 2010
127  \item \alert{A canonical locally nameless formalisation of an algebraic logical
128    framework}, talk given by Wilmer Ricciotti at Types 2010, Warsaw
129    (13 October 2010)
130 \end{itemize}
131\end{frame}
132
133\begin{frame}
134 \frametitle{Dissemination activity}
135 List of presentations given to \alert{inviting institutions}:
136 \begin{itemize}
137  \item \alert{Certifying cost annotations in compilers}, talk given by Nicolas Ayache
138   at the LIP6 laboratory of the University Paris 6 (18 November 2010)
139  \item \alert{A canonically nameless representation of binders}, talk given by Randy Pollack at U. Penn at Philadelphia (11 June 2010)
140  \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)
141  \item \alert{Certifying cost annotations in compilers}, talk given by Roberto Amadio at ENS/Lyon.
142 \end{itemize}
143\end{frame}
144
145\begin{frame}
146 \frametitle{Dissemination activity}
147 \alert{Other seminars:}
148 \begin{itemize}
149  \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)
150 \end{itemize}
151\end{frame}
152
153\begin{frame}
154 \frametitle{Dissemination activity}
155 Papers \alert{currently submitted:}
156 \begin{itemize}
157  \item \alert{An executable formalisation of the MCS-51 microprocessor in Matita}, Dominic Mulligan and Claudio Sacerdoti Coen. Submitted to Interactive Theorem Proving 2011
158  \item \alert{Certified complexity}, Dominic Mulligan and Claudio Sacerdoti Coen. Poster submission at FET11
159  \item \alert{The Matita Interactive Theorem Prover}, Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico Tassi. System description submitted to CADE 2011
160  \item \alert{Certifying cost annotations in compilers}, Roberto Amadio, Nicolas Ayache, Yann Regis-Gianas, Ronan Saillard. Submitted to Formal Methods 2011
161  \item \alert{Elementary affine lambda-calculus with multithreading and side effects}, A. Madet, R. Amadio. Submitted to TLCA 2011
162  \item \alert{A decompilation of the pi-calculus and its applications to termination}, Roberto Amadio. Submitted to ICALP 2011.
163 \end{itemize}
164\end{frame}
165
166\end{document}
Note: See TracBrowser for help on using the repository browser.