GT Scalp (Structures formelles pour le CALcul et les Preuves)

Actualités du GT Scalp

Présentation

L’objectif du GT Scalp (Structures formelles pour le CALcul et les Preuves) du GdR IM est d'animer la communauté des chercheurs français travaillant sur les structures mathématiques permettant de modéliser preuves et programmes, avec une attention particulière (mais non exclusive) à l'interface entre les deux. Le spectre du groupe, qui s'insère dans un éventail de disciplines allant de la théorie de la démonstration à la théorie des langages de programmation, couvre notamment les systèmes de calcul d'origine logico-algébrique (lambda-calcul, réécriture de termes et de graphes, calculs de processus), les systèmes de déduction logique (classique, intuitionniste, linéaire), la théorie des types et les systèmes d'inférence, ainsi que les outils de preuve automatiques ou interactifs, avec des applications à l'analyse et la vérification de programmes (interprétation abstraite, logiques de programmes, automates d'arbres) et de leurs propriétés quantitatives (analyse de complexité, analyse de programmes probabilistes ou quantiques, complexité algorithmique implicite). Les méthodes employées sont à la fois de nature syntaxique (séquents, systèmes de types, machines abstraites, induction et coinduction, recherche de preuves) et sémantique (catégories, domaines, jeux, espaces vectoriels, réalisabilité).

Le groupe Scalp est susceptible d’avoir des interactions fécondes avec les groupes LTP du GDR GPL pour les applications à l'analyse des programmes, et LHC du GDR IM pour les fondements des outils mathématiques employés.

Origine du GT Scalp

Tout comme le groupe de travail LHC, le GT Scalp hérite des groupes de travail LAC et GeoCal, et est le résultat d'une réorganisation de ces deux groupes, de renouvellements thématiques et de l'apport de nouveaux membres faisant suite à une réflexion engagée à l'occasion des journées annuelles communes des deux groupes LAC et GEOCAL en 2016.

L'objectif de cette restructuration est d'améliorer la lisibilité thématique de nos groupes au sein du GDR-IM et vis-à-vis du reste de la communauté informatique, pour clarifier les communautés visées, plus clairement définir les domaines mathématiques mobilisés et améliorer la perméabilité avec d'autres GDR.

Organisation de Scalp

Responsables du GT

Liste de diffusion

À venir (les listes des GT Geocal et LAC sont encore actives pour le moment).

Laboratoires et équipes impliqués dans le GT Scalp

À venir.