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.