Open invitation - Registration Required - Please register before January 21st.
PROGRAM
09:30 Registration
10:00 Welcome Address
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 and proof language based on temporal logic, where first-order logic and set theory are used to describe a set of states and the possible transitions between these states. TLA+ also includes a module system for manipulating large-scale specifications
12:30 Lunch
14:00 Dynamic Dictionary of Mathematical Functions
Bruno Salvy, INRIA
-
The project "Dynamic Dictionary of Mathematical Functions" 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 the 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
16:30 Demos and Cocktails
More Information and registration :
+33 1 69 35 69 70
