Institut de Mathématiques de Marseille, UMR 7373




Rechercher


Accueil > Équipes de recherche > Logique de la Programmation (LDP) > Thèmes de l’équipe

Thèmes de l’équipe

par Lozingot Eric - publié le , mis à jour le

L’équipe Logique De la Programmation (LDP) fut fondée par Jean-Yves Girard en 1992. Les thèmes traditionnels de l’équipe portent sur la théorie de la démonstration, la logique linéaire, la sémantique dénotationnelle, le lambda-calcul. Plus récemment l’équipe s’est ouverte sur de nouvelles thématiques, notamment la théorie de la réécriture, les langages concurrents, le lambda-calcul différentiel, la théorie homotopique des types, la réalisabilité.

  • Théorie de la démonstration

Une réflexion sur les principaux axes de la logique, en proposant de remplacer le réalisme axiomatique par un maillage de type kantien fondé sur quatre cases cognitives : constat, performance, usine, usage. Ce qui recoupe les distinctions apparues après 1930 : implicite/explicite (= a priori/a posteriori) et pur/typé (= analytique/synthétique) ; ainsi, l’usine correspond-elle au synthétique a posteriori, celui des réseaux de démonstration.

Chercheur : Jean-Yves Girard
Interactions : Michele Abrusci (Roma 3)

  • Sémantique quantitative : logique linéaire et non-déterminisme calculatoire

Les sémantiques quantitatives sont une classe de modèles dénotationnels de la logique linéaire et du λ-calcul, dans lesquels les termes sont interprétés par des combinaisons linéaires formelles d’atomes, ces derniers pouvant être vus comme des approximations finies de termes en forme normale. Le cas emblématique est le modèle des foncteurs normaux introduit par Girard, et qui servit de base à l’introduction des espaces cohérents, puis de la logique linéaire, dans les années 1980.

Cette ligne de travail connait un renouveau depuis début des années 2000, initié par les travaux d’Ehrhard et Regnier qui, à partir des propriétés des modèles quantitatifs, ont introduit les concepts de logique linéaire différentielle et de développement de Taylor des λ-termes. Ces idées sont la base de nombreuses avancées récentes, avec par exemple des caractérisations de propriétés opérationnelles quantitatives (probabilité de normalisation, comptage de chemins de réduction, etc.).

Chercheurs : Lionel Vaux
Thésards : Thomas Leventis, Jules Chouquet (ANR Rapido, Paris Diderot)
Interactions : Thomas Ehrhard, Michele Pagani, Christine Tasson (IRIF, Paris Diderot), Ugo Dal Lago (Bologne), Jim Laird (Bath), Giulio Guerrieri

  • Sémantique des langages concurrents

Pour la modélisation des systèmes concurrents, de nombreux langages formels ont été proposés (CSP, CCS, pi-calcul, et leurs extensions), mais aucun ne peut se prévaloir d’être le point de référence consensuel comme l’est le lambda-calcul dans le cadre fonctionnel ; de façon similaire, il n’y a pas de notion unique de ce que devrait être un modèle pour de tels langages. Nous développons des approches à ce problème fondées sur la théorie de la démonstration en exploitant notamment les développements sémantiques qui permettent de traiter explicitement de l’interaction et du non-déterminisme tant du point de vue des langages que des modèles associés : géométrie de l’interaction, logique différentielle et modèles quantitatifs, jeux concurrents et structures d’événements, constructions par orthogonalité, etc. Cette
étude mène à étendre et questionner la correspondance entre preuves et programmes dans le cadre concurrent.

Chercheur : Emmanuel Beffara
Interactions : Olivier Laurent (LIP, ENS Lyon) Virgile Mogbil (LIPN, Paris Nord) Claudia Faggian (IRIF, Paris Diderot) Daniel Hirschkoff (LIP, ENS Lyon) Tom Hirschowitz (LAMA, Savoie) Daniele Varacca (LACL, Créteil).

  • Ludique : théorie formelle des dialogues et de l’argumentation

Construction de nouveaux connecteurs logiques.

Chercheur : Myriam Quatrini

  • Catégories supérieures, algèbre homotopique et réécriture

Les catégories et groupoïdes de dimension supérieure sont une généralisation des monoïdes et des groupes, qui apparaissent naturellement en topologie algébrique, mais aussi en logique et théorie du calcul. Les pistes développées au sein de l’équipe vont de la théorie des invariants homologiques et homotopiques de la réécriture, initiée par Anick et Squier, à l’étude des types d’homotopie via les catégories supérieures, en passant par la combinatoire des catégories supérieures, notamment celle des orientaux de Street, par l’étude des diagrammes de cohérence et par celle des différents modèles algébriques et homotopiques des catégories supérieures, dans la lignée de Quillen, Thomason et Grothendieck.

Chercheurs : Dimitri Ara, Yves Lafont
Thésards : Matteo Acclavio, Andrea Gagna
Réseau de recherche : ANR CATHRE (Catégories, Homotopie et Réécriture)
Collaborateurs : Albert Burroni (IRIF, Paris Diderot), Denis-Charles Cisinski (IMT, Toulouse), Patrick Dehornoy (LMNO, Caen & IRIF, Paris Diderot), Moritz Groth (Friedrich-Wilhelms-Universität, Bonn), Javier J. Gutiérrez (Universitat de Barcelona), Georges Maltsiniotis (IMJ, Paris Diderot), François Métayer (IRIF, Paris Diderot), Ieke Moerdijk (Universiteit Utrecht), Krzysztof Worytkiewicz (LAMA, Savoie)

  • Réalisabilité classique

La réalisabilité classique de Jean-Louis Krivine est une extension à la logique classique de la réalisabilité de Kleene qui peut être vue comme une généralisation de la méthode de forcing de Cohen dans laquelle les formules de la théorie des ensembles de Zermelo-Fraenkel sont réalisées par des programmes (des lambda-termes). La théorie se développe autour de deux grands thèmes :
- la question de la spécification : étant donnée une formule (de ZF) quel est le comportement des programmes réalisant celles-ci ? Et réciproquement étant donnée une spécification de programme, peut-on trouver une formule telle que les programmes satisfaisant cette spécification sont exactement ceux réalisant la formule ?
- l’étude des modèles de réalisabilité : l’ensemble des formules réalisées forme un théorie cohérente qui par complétude possède donc un modèle ; on peut construire ainsi des modèles nouveaux de ZF.

Chercheur : Laurent Regnier
Thésard : Guillaume Geoffroy
Interactions : Jean-Louis Krivine, Alexandre Miquel (PPS, Paris 7), Pierre Hyvernat, Christophe Raffali (LAMA, Chambéry), Thomas Streicher (Darmstadt).
-
-
-