Open invitation - Registration Required - See here for late Registration.


09:00    Registration

09:30    Welcome Address
Andrew Blake, Managing Director, Microsoft Research Cambridge
Michel Cosnard, CEO, INRIA

09:45    Mathematical Components
Assia Mahboubi, INRIA

  1. 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 a significant development: the historical proof of the Odd Order theorem.

10:10    Secure Distributed Computations and their Proofs
Cédric Fournet, Microsoft Research Cambridge

  1. 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.

10:35    Break

11:00    TLA+
Damien Doligez, INRIA

  1. 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.

11:25    Dynamic Dictionary of Mathematical Functions
Frédéric Chyzak, INRIA

  1. 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.

11:50    A-Brain
Gabriel Antoniu, INRIA
Bertrand Thirion, INRIA

  1. Joint acquisition of neuroimaging and genetic data on large cohorts of subjects is a new approach used to assess and understand the variability that exists between individuals, and that has remained poorly understood so far. As both neuroimaging- and genetic-domain observations represent a huge amount of variables, performing statistically rigorous analyses on such amounts of data represents a computational challenge that cannot be addressed with conventional computational techniques. The project investigates the benefits of integrating BlobSeer, a scalable cloud data management system, developed by the Kerdata INRIA team, with Microsoft Azure storage services and aims at evaluating the impact of using BlobSeer on Azure with large-scale application experiments such as the genetics-neuroimaging data comparisons addressed by the Parietal INRIA team.

12:15    Lunch and Demos

14:00    ReActivity
Jean-Daniel Fekete, INRIA

  1. 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.

14:25    Adaptive Combinatorial Search for e-Sciences
Youssef Hamadi, Microsoft Research Cambridge
Marc Schoenauer, INRIA

  1. 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.

14:50    Scientific Image and Video Data Mining
Jean Ponce, Ecole Normale Supérieure

  1. 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.

15:15    Break and Demos

16:00    Panel on Formal Methods
Chirstine Paulin (Paris-Sud), Cédric Fournet (Microsoft
Research Cambridge), Tony Hoare (Microsoft Research Cambridge),
Peter Paule (J.Kepler University, Linz), David Pointcheval (Ecole
Normale Supérieure), Mark Ryan (University of Birmingham), Wolfram
(Microsoft Research Redmond); Jean-Jacques Lévy (INRIA,
Director of the Microsoft Research-INRIA Joint Centre).

17:00    Demos and Cocktails

More Information and registration :

+33 1 69 35 69 70