L’équipe Logique de la Programmation est une équipe de recherche de l’Institut de Mathématiques de Luminy, UMR 6206 du CNRS. Fondée par Jean-Yves Girard en 1992, l’équipe LDP fait porter sa recherche sur la logique mathématique, la théorie de la démonstration et la théorie du calcul, ainsi que sur les interactions entre ces théories et d’autres disciplines, notamment les mathématiques, l’informatique, la linguistique, la philosophie et la biologie.

L’équipe a de nombreuses collaborations avec des laboratoires en France (Marseille, Paris, Montpellier, Sophia-Antipolis, Grenoble, Chambéry, Nancy) et à l’étranger (Italie, Royaume-Uni, Allemagne, Canada, Etats-Unis, Japon). Au niveau local elle participe aux activités de la FRUMAM, et organise un groupe de travail avec des chercheurs du LIF.

Elle coordonne l’ACI Géométrie du Calcul, et participe à l’AS Topologie Algébrique pour l’étude des structures de calcul, et notamment de la concurrence, au Master Recherche de Mathématiques Discrètes et Fondements de l’Informatique et au Master Professionnel de Mathématiques et Informatique des Nouvelles Technologies.

Sur le plan scientifique l’équipe s’est récemment ouverte à de nouveaux champs d’application : théorie homotopique du calcul, combinatoire des relations, vérification automatique, logique et philosophie, systèmes discrets et biologie. Le paradigme initial est la correspondance de Curry-Howard, qui relie preuves et formules logiques aux concepts informatiques de programmes (termes du lambda-calcul) et types. Ce paradigme est à l’origine d’un grand nombre de développements (notamment la logique linéaire de Girard), sujets de recherche pour plusieurs membres de LDP.