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

L'EJCIFM se déroulera à Caen du 16 au 20 juin 2025, avec au menu du ZX-calcul, du calcul en virgule flottante, de la combinatoire énumérative sur les diagrammes de cordes et un cours sur la compilation de connaissances, et un cours de sémantique dénotationelle et des jeux par Pierre Clairambault.
l'EPIT 2025 se déroulera à Aussois du 19 au 23 mai 2025, sur le thème du raisonnement (co)inductif & circulaire et de son application à la programmation, la preuve formelle et la vérification logicielle.
Les journées nationales 2025 du GRD-IFM se sont tenues à Bordeaux la dernière semaine de mars.
Les rencontres 2024 du GT Scalp ont été organisées à Lille conjointement avec le GT Vérif. Elles se sont déroulées du 18 au 21 novembre 2024.
Les journées annuelles d'informatique mathématique se sont tenues à Grenoble du 18 au 21 mars 2024.
À l'occasion des JNIM 2024 se tiendra une demi-journée thématique sur les assistants de preuves, le 19 mars après-midi à Grenoble. Au programme des exposés pléniers de Christine Paulin (LMF) et Pierre-Marie Pédrot (LS2N) et une table ronde sur l'utilisation des assistants de preuves dans l'enseignement, où interviendront Riccardo Brasca (IMJ-PRG), Julien Narboux (ICUBE), Micaela Mayero (LIPN, sous réserve), Pierre Rousselin (LAGA) et Yannick Zakowski (LIP).
En janvier 2024, le GDR-IM devient GDR IFM: informatique fondamentale et ses mathématiques.

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 LVP et CLAP du GDR GPL pour les applications à l'analyse des programmes et la compilation, 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.

Responsables du GT

Liste de diffusion

Liste de diffusion du GT Scalp: gt-scalp_à_gdr-ifm.fr.

Informations et recommandations du GDR IM sur l'usage des mailing-lists.

Pour vous inscrire sur la liste de diffusion, veuillez suivre la procédure suivante:

1. Allez sur https://mygdr.hosted.lip6.fr/

2. Cliquez sur « Laboratoires » afin de vérifier que votre laboratoire est présent dans la base. Attention : Si vous n'êtes affilié à aucun laboratoire français, mais uniquement à une institution à l'étranger, vous devrez utiliser « Laboratoire à l'étranger ». - Si votre laboratoire est présent dans la base, alors passez au point 3. - Sinon, merci de nous le signaler (à Damiano ou Alexis) car vous ne pouvez pas vous inscrire. A cette fin, nous envoyer le nom complet de votre laboratoire, son acronyme, et son adresse web. Nous rajouterons votre laboratoire dans la liste, et nous vous signalerons lorsque ce sera fait, afin que vous puissiez vous inscrire.

3. Cliquer sur « S’inscrire », et procéder à l’inscription (email professionnel de préférence) en respectant les consignes de création de mot de passe, et en mémorisant vos login et mot de passe.

4. Connectez vous avec votre nom de login de votre mot de passe.

5. Remplir votre fiche.

6. Cliquer sur « IM », et la liste des GT apparait. Sélectionnez le ou les GTs auxquels vous appartenez, et c’est (presque) fini.

7. Jusqu'à nouvel ordre, envoyez dans la foulée un email à Alexis pour indiquer que vous vous êtes inscrits au GT.

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

Actualités du GT Scalp

Présentation

Origine du GT Scalp

Organisation de Scalp

Responsables du GT

Liste de diffusion

Archives