|
Jean-Jacques Lévy
|
tarix | 05.10.2018 | ölçüsü | 9,45 Mb. | | #72322 |
|
Jean-Jacques Lévy Jean-Jacques Lévy IKI, June 11, 2008
Plan Context Track A Track B - DDMF
- ReActivity
- Adaptative search
- Image & video mining
Context
Management
Long cooperation among researchers
Organization
Localization
PhD Students
Track A
Mathematical components Computational proofs - computer assistance for long formal proofs.
- reflection of computations into Coq-logic: ssreflect.
Secure Distributed Computations and their Proofs Distributed computations + Security - programming with secured communications
- certified compiler from high-level primitives to low-level crypto-protocols
- formal proofs of probabilistic protocols
Secure Distributed Computations and their Proofs Recent results: - secure sessions v2 (proofs by typing)
- concurrent secure sessions v1
- correctness proofs of TLS implementations
- information flow + cryptography
- secure logs
- secure modeling of e-cash
Natural proofs - first-order set theory + temporal logic
- specification/verification of concurrent programs.
- tools for automatic theorem proving
Tools for formal proofs Recent results: - Proof Manager with incremental, non-linear proofs
- declarative meta-language
- proofs like done by Mathematicians
- proof of the atomic Bakery algorithm with PM
Track B Scientific Information Interaction
Dynamic dictionary of math functions - dynamic tables of their properties.
- generation of programs to compute them.
ReActivity Logs of experiments for biologists, historians, other scientists - mixed inputs from lab notebooks and computers,
- interactive visualization of scientific activity,
- support for managing scientific workflow.
ReActivity Recent results: - workshop on Interacting with Temporal Data at CHI’09 (35 participants)
- streamlining the computation of aggregated metrics on Wikipedia “live” and small focused “Dashboard visualizations” tools
- WILD: Wall-sized Interaction with Large Datasets (32 screens, 8 Vicon, 1 interactive table expansions)
- Augmented Paper/Electronic Notebooks
Adaptive Combinatorial Search for E-science Parallel constraint programming and optimization for very large scientific data - improve the usability of Combinatorial Search algorithms.
- automate the fine tuning of solver parameters.
- parallel solver: “disolver”
Computer vision and Machine learning for: - sociology: human activity modeling and recognition in video archives
- archaeology and cultural heritage preservation: 3D object modeling and recognition from historical paintings and photographs
- environmental sciences: change detection in dynamic satellite imagery
Future
Objectives - 30 resident researchers
- tight links with French academia (phD, post-doc)
- develop useful research for scientific community
- provide public tools (BSD-like license)
- become a new and attractive pole in CS research
- and source of spin off companies
Dostları ilə paylaş: |
|
|