GDR Informatique Mathématique : Groupe de travail Geocal

Responsable : Laurent Regnier, Institut de Mathématiques de Luminy

Annonces du groupe

Présentation

Le groupe Géométrie du calcul s'inscrit dans la continuation du projet Geocal (ACI Nouvelles interfaces des mathématiques) qui a existé de 2003 à 2006, et dont il prolonge les principales thématiques. La problématique générale est de trouver au sein de la logique et des mathématiques des outils permettant la modélisation abstraite des programmes. Un exemple spectaculaire du succès de cette approche est l'invention de la logique linéaire issue d'une part de l'isomorphisme de Curry-Howard établissant la correspondance entre les déductions formelles en logique intuitionniste et le lambda-calcul typé, et d'autre part de la modélisation du lambda-calcul par des espaces présentant des analogies fortes avec les espaces vectoriels.

Dans ce cadre général le groupe poursuivra notamment mais non exclusivement les objectifs suivants :

poursuivre les travaux sur la correspondance preuve/programme, avec deux sous-objectifs majeurs : étudier les sémantiques de réalisabilité qui posent le problème profond de comprendre le sens opérationnel des énoncés mathématiques, et étendre les systèmes logiques de typage à des langage plus expressifs que le simple lambda-calcul, typiquement les calculs parallèles ;
poursuivre les travaux en complexité implicite visant à représenter des classes de complexité algorithmique par des contraintes logiques (logique linéaire légère, Bellantoni-Cook) ;
développer le cadre topologique pour la concurrence et la géométrie de la réécriture dans la lignée des travaux sur l'homotopie dirigée qui fournissent un cadre très élégant pour raisonner sur les problèmes de synchronisation entre processus ;
explorer certaines pistes particulièrement prometteuses et récemment apparues donnant à penser qu'une unification conceptuelle est possible entre les paradigmes de calcul séquentiel (lambda-calcul) et parallèle (pi-calcul) : citons en particulier les rapprochements entre la sémantique des jeux et les systèmes de transitions vus comme jeux positionnels, et les analogies entre le lambda-calcul différentiel et le calcul avec resources.

Participants

IML (Marseille)
Emmanuel Beffara
Yves Lafont
Laurent Regnier
Lionel Vaux
doctorants
Pierre Rannou
Thomas Seiller
LIF (Marseille)
Luigi Santocanale
Mimosa (Sophia-Antipolis)
Gérard Boudol
IRIT (Toulouse)
Serguei Soloviev
LIP (Lyon)
Philippe Audebaud
Patrick Baillot
Jean Duprat
Daniel Hirschkoff
Olivier Laurent
Pierre Lescanne
Colin Riba
postdoc
Paolo Tranquili
doctorants
Marc Lasson
Romain Demangeon
Aurélien Pardon
Barbara Petit
ICJ (Lyon)
Philippe Malbos
LAMA (Chambery)
Noël Bernard
René David
Tom Hirschowitz
Pierre Hyvernat
Karim Nour
Christophe Raffalli
doctorants
Florian Hatat
Muhammad Humayoun
Calligramme (Nancy)
Philippe de Groote
François Lamarche
Carte (Nancy)
Jean-Yves Marion
Protheo (Nancy)
Yves Guiraud
PPS (Paris)
Antonio Bucciarelli
Albert Burroni
Pierre-Louis Curien
Thomas Ehrhard
Philippe Gaucher
Jean-Louis Krivine
Paul-André Melliès
François Métayer
postdoc
Marc Defalco
doctorants
Pierre Clairambault
Mehdi Dogguy
Jonas Frey
Stéphane Gimenez
Alexi Goyet
Guillaume Munch Maccagnoni
Christine Tasson
Stéphane Zimmermann
LIPN (Villetaneuse)
Pierre Boudes
Christophe Fouqueré
Damiano Mazza
Virgile Mogbil
Michele Pagani
Jacqueline Vauzeilles
associé
Ugo Dal Lago
LSV (Cachan)
Jean Goubault-Larrecq
Étienne Lozes
CEA (Saclay)
Eric Goubault
Emmanuel Haucourt
Michel Hirschowitz
postdoc
Samuel Mimram
LogiCal (Palaiseau)
Hugo Herbelin
UNSA (Sophia-Antipolis)
André Hirschowitz
doctorants
Julianna Zsido
Benedikt Ahrens
Pierre Abbrugiati
SARDES (Saint-Ismier)
Damien Pous
EMN (Nantes)
Nicolas Tabareau
LaBRI (Bordeaux)
Christian Retoré