GT LHC

Depuis quelques décennies, des rapprochements profonds ont été établis entre certains concepts et outils de l’informatique théorique (logique, réécriture, etc.) et ceux issus de la topologie (théorie de l’homotopie, topologie algébrique, etc.), en utilisant les catégories comme langage commun (topos, catégories de modèles, etc.).

L’objectif du groupe LHC est de rassembler, d’animer et de représenter la communauté française de chercheurs travaillant à développer et exploiter ces liens, ou cherchant à en établir de nouveaux, en vue d’étudier les fondations théoriques des langages de programmation, de la logique, et de leurs sémantiques.

Représenter de manière effective les structures mathématiques en jeu, c’est-à-dire en donner le langage interne, permet de faciliter le raisonnement sur ces structures (c’est le programme de la théorie homotopique des types), voire de résoudre des problèmes par le calcul (d’invariants homologiques, par exemple).

Réciproquement, ces structures enrichissent le paysage des modèles mathématiques de la logique et du calcul, guidant la généralisation de concepts d’informatique théorique bien établis (réécriture en dimension supérieure, par exemple), ou la mise au point de nouveaux outils syntaxiques (la représentation explicite des ressources en lambda-calcul, via la notion de dérivée formelle).