Open invitation - Registration Required - See here for late Registration.
PROGRAM
09:30 Registration
10:00 Welcome Address
Général Xavier Michel, Directeur Général de l’École Polytechnique
Michel Cosnard, CEO, INRIA
Andrew Herbert, Managing Director, Microsoft Research Cambridge
10:45 Mathematical Components
Georges Gonthier, Microsoft Research Cambridge
-
Formalized mathematical theories can, like modern software, be built out of components. By components we mean modules that comprise both the static (objects and facts) and dynamic (proof and computation methods) contents of theories. We develop a general platform for mathematical components, based on the Coq "ssreflect" extension that was used to carry out the formalization of the Four Colour Theorem. We would validate the platform on two significant developments: a theory of efficient arithmetic, and the proof of the Odd Order theorem.
11:15 Break
11:30 Secure Distributed Computations and their Proofs
Cédric Fournet, Microsoft Research Cambridge
-
We present programming tools for building distributed applications with strong security guarantees. Given some security goals and attacker model, our tools produce executable code and their security proof. In particular, they generate and verify cryptographic protocols to protect the application, even when large parts of the computation are controlled by the attacker. We illustrate our approach on multiparty sessions, information-flow security, and the TLS protocol.
12:00 TLA+
Damien Doligez, INRIA
-
TLA+ is a specification language especially suited to describing and formally specifying concurrent and distributed systems. TLA+2 is the next version of TLA+, which adds a proof language that allows writing formal proofs of correctness of systems specified in TLA+. In addition to TLA+2, we will present the tools we are developing to help engineers write and certify proofs in TLA+2.
12:30 Lunch and Demos
14:00 Dynamic Dictionary of Mathematical Functions
Bruno Salvy, INRIA
-
The project aims at providing a web encyclopedia of mathematical functions that is completely computer generated. The framework is given by computer algebra algorithms for solutions of linear differential equations. While developing new algorithms in this area, we also started to work on defining a language for developing dynamic mathematics on the web. In this talk, we give an overview of our aims, our methods and a short demo of our prototype.
14:30 ReActivity
Jean-Daniel Fekete, INRIA - Wendy Mackay, INRIA
-
The goal is to explore how to capture and visualize user activity, to enable scientists and groups of scientists to reflect upon, and to interact with and improve their research processes. We intend to develop sophisticated strategies for logging activity with bilateral links between on-line and off-line data, and powerful methods for visualising across multiple scales and interacting with the results.
15:00 Break
15:15 Adaptative Combinatorial Search for e-Sciences
Youssef Hamadi, Microsoft Research Cambridge
Marc Schoenauer, INRIA
-
Adaptive Search is concerned with automatic tuning of parameters in search algorithms. Three different types of algorithms have been already addressed by our project: an innovative Constraint Programming heuristic which adapts to the observed performance of past decisions; an Adaptive Operator Selection in Evolutionary Algorithms with Multi-Armed Bandit techniques; and a variation on the Covariance Matrix Adaptation Evolution Strategy (either specializing or generalizing its adaptive scheme) in the context of continuous optimization.
15:45 Scientific Image and Video Data Mining
Jean Ponce, Ecole Normale Supérieure
-
Our research is about mining dynamical remote data with applications in computational ecology and environmental science, mining historical collections of photographs and paintings with applications to archaeology and cultural heritage preservation, and mining TV broadcasts with applications to sociology
16:15 Conclusion
Jean-Jacques Lévy, Director, Microsoft Research-INRIA Joint Centre
Table ronde ``Partenariat Recherche Publique, Recherche Privée’’
Michel Cosnard, Jean-Jacques Lévy,
Eric Boustouller, CEO, Microsoft France,
Tony Hey, Corporate Vice President of External Research, Microsoft,
Geneviève Fioraso, Députée de l’Isère,
Pierre Lasbordes, Député de l’Essonne,
Mateo Valero, Director, Barcelona Supercomputing Center.
17:45 Closing remarks
Luc Rousseau, directeur de la DGE
17:55 Demos and Cocktails
More Information and registration :
+33 1 69 35 69 70
