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

Last change on this file since 1839 was 1839, checked in by sacerdot, 8 years ago

...

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