Jean-Jacques Lévy



Yüklə 9,45 Mb.
tarix05.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

  • 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


Tools for formal proofs

  • 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

  • Computational Sciences

  • Scientific Information Interaction



Dynamic dictionary of math functions













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”




Image and video mining for science and humanities

  • 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


Sciences in track B



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




Yüklə 9,45 Mb.

Dostları ilə paylaş:




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2024
rəhbərliyinə müraciət

    Ana səhifə