- home
- projects
projects
Secure Distributed Computations and their Proofs
We intend to design formal tools for programming distributed computation with effective security guarantees. Our goal is to enable the programmer to express and prove high-level security properties with a reasonable amount of effort---sometimes automatically, sometimes with mechanical assistance---as part of the development process. These properties should hold in a hostile environment, with realistic (partial) trust assumptions on the principals and machines involved in the computation.
Mathematical Components
The object of this project is to demonstrate that 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 propose to 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.
Tools and Methodologies for Formal Specifications and for Proofs
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.
Dynamic Dictionary of Mathematical Functions
We intend to show that a large part of the code concerning elementary and special functions with computer algebra systems can actually be generated automatically in a uniform way. We start by giving linear differential and difference equations the status of data structures that represent their solutions. New efficient algorithms operating directly on this data structure will be designed in this project. We intend to develop a dictionary of special functions, available on the web, that will be the showcase of this project. In addition to our existing prototype, this new version will offer dynamical entries depending on user requests, integral transforms (Laplace, Fourier,...) and more information concerning each function. To achieve the desired efficiency, the project contains a strong theoretical investment on the complexity of fundamental algorithms in computer algebra.
Adaptive Combinatorial Search for e-Sciences
Our research project aims at improving the usability of modern optimization methods (also called search algorithms). We are located in Orsay, within the Microsoft Research-INRIA Joint Centre, with participants from the Constraint Reasoning Group at Microsoft Research Cambridge, and the TAO project at INRIA Futurs. Please contact us for additional information, visits, internships, etc.
ReActivity
The goal of this project is to explore how to capture and visualize user activity, enabling scientists to reflect upon, interact with and improve their research processes. We are located in Orsay, with participants from the Aviz and inSitu research teams at INRIA Saclay-Ile de France and the VIBE project at Microsoft Research Redmond.
Scientific Image and Video Data Mining
We propose to focus on fundamental computer science research in computer vision and machine learning, and its application to archaeology, cultural heritage preservation, environmental science, and sociology. We validate our project by collaborations with researchers and practitioners in these fields.