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

Last change on this file since 1837 was 1837, checked in by boender, 8 years ago
  • added first draft of WP6 presentation
File size: 6.2 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 16, 2012}
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] Project Web Site and Software Repository
66 \item[D6.2] 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 was due in the second period.
73\end{frame}
74
75\begin{frame}
76 \frametitle{Dissemination activity}
77 Presentations given to \alert{international conferences}:
78
79        \small
80\begin{itemize}
81        \item \alert{Certified Complexity}, talk given by Claudio Sacerdoti Coen at
82        Types 2010, Warsaw (15 October 2010).
83        \item \alert{Realizability Models for Cost-Preserving Compiler Correctness},
84        talk given by Marco Gaboardi at DICE 2010.
85        \item \alert{A canonical locally nameless formalisation of an algebraic
86        logical framework}, talk given by Wilmer Ricciotti at Types 2010, Warsaw (13
87        October 2010).
88        \item \alert{An Elementary Affine $\lambda$-Calculus with Multithreading and
89        Side Effects}, talk given by A.  Madet at TLCA 2011 (2 June 2011)
90        \item \alert{A type system for positivity}, talk given by Claudio Sacerdoti
91        Coen at Types 2011 (10 September 2011)
92        \item \alert{The Matita Interactive Theorem Prover}, talk given by Wilmer
93        Ricciotti at CADE 2011 (3 August 2011)
94\end{itemize}
95\end{frame}
96
97\begin{frame}
98 \frametitle{Dissemination activity}
99        Posters presented at \alert{international conferences}:
100
101        \small
102        \begin{itemize}
103                \item \alert{Certified Complexity}. Poster presented by Claudio Sacerdoti
104                Coen and Dominic Mulligan at FET 2011, Budapest (4--6 May 2011).
105        \end{itemize}
106\end{frame}
107 
108\begin{frame}
109 \frametitle{Dissemination activity}
110 Presentations given to \alert{inviting institutions}:
111\small
112\begin{itemize}
113        \item \alert{Certifying cost annotations in compilers}, talk given by Nicolas
114        Ayache at the LIP6 laboratory of the University Paris 6 (18 November 2010);
115        \item \alert{A canonically nameless representation of binders}, talk given by
116        Randy Pollack at U.  Penn at Philadelphia (11 June 2010);
117        \item \alert{A canonically nameless representations of binders}, talk given by
118        Randy Pollack at Lab PPS (Paris) to the INRIA-Rocquencourt team $\pi$ r2
119        26 November 2010);
120        \item \alert{Certifying cost annotations in compilers}, talk given by Roberto
121        Amadio at ENS/Lyon.
122        \item \alert{Certified Complexity}, talk given by Claudio Sacerdoti Coen at
123        the University of Birmingham (20 December 2011).
124        \item \alert{Certifying cost annotations in compilers}, talk given by Nicolas
125        Ayache at ENSTA (13 December 2011);
126\end{itemize}
127\end{frame}
128
129\begin{frame}
130 \frametitle{Dissemination activity}
131 \alert{Other seminars:}
132        \small
133\begin{itemize}
134        \item \alert{Operational Semantics in Specifications}, talk given by Brian
135        Campbell at the Laboratory for Foundations of Computer Science, University of
136        Edinburgh (16 March 2010)
137        \item \alert{An executable semantics for CompCert C}, talk given by Brian
138        Campbell at the Scottish Programming Language seminar at Heriot-Watt
139        University (11 November 2011).
140\end{itemize}
141\end{frame}
142
143\begin{frame}
144 \frametitle{Dissemination activity}
145 Papers \alert{published}:
146\small
147\begin{itemize}
148        \item \alert{A Canonical Locally Named Representation of Binding}, R. Pollack,
149        M. Sato and W.  Ricciotti, Journal of Automated Reasoning
150        \item \alert{Certifying and reasoning on cost annotations of functional
151        programs}, R.M. Amadio, Y.Regis-Gianas, Proceedings of FOPARA 2011
152        \item \alert{An Elementary Affine $\lambda$-Calculus with Multithreading and
153        Side Effects}, A. Madet, R.M. Amadio, Proceedings of TLCA 2011
154        \item \alert{Certified Complexity}, R. Armadio, A. Asperti, N. Ayache, B.
155        Campbell, D. Mulligan, R.  Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I.
156        Stark, in Proceedings of FET 11
157        \item \alert{The Matita Interactive Theorem Prover}, A.Asperti, W.Ricciotti,
158        C. Sacerdoti Coen, E.Tassi, In Automated Deduction – CADE-23, Lecture Notes
159        in Computer Science
160\end{itemize}
161\end{frame}
162
163\begin{frame}
164 \frametitle{Dissemination activity}
165 Papers \alert{currently submitted:}
166\small
167\begin{itemize}
168        \item \alert{An executable formalisation of the MCS-51 microprocessor in
169        Matita}, Dominic Mulligan and Claudio Sacerdoti Coen.
170        \item \alert{On the correctness of an assembler for the Intel MCS-51
171        microprocessor}, Dominic Mulligan and Claudio Sacerdoti Coen.
172        \item \alert{Certifying cost annotations in compilers}, Roberto Amadio,
173        Nicolas Ayache, Yann Regis-Gianas, Ronan Saillard.
174        \item \alert{An executable semantics for CompCert C}, Brian Campbell. To be
175        submitted for the first time this year.
176\end{itemize}
177\end{frame}
178
179\end{document}
Note: See TracBrowser for help on using the repository browser.