• Point logistique
• Retour sur la création du GT
• Préparation et participation aux Journées
• Discussion sur le périmètre du GT
• Discussion sur les actions à conduire dans le GT
• Journées annuelles 2019
• Questions diverses

Plan pour le dîner

• Discussion sur l'avenir des GT a débuté lors des journées communes GeoCal-LAC de 2016 à l'IRIF
• Discussions avec la direction du GDR-IM en novembre 2017
• Proposition de nouveaux GT présentées et discutées aux journées 2017 à Nantes
• Avril 2018: proposition du texte de présentation des GT LHC et Scalp
• Été 2018: Validation des nouveau GT
• Fin septembre 2018: Création des nouvelles listes de diffusion
• Responsables du GT: Thibaut B, Damiano M, Alexis S

• Page des journéess
• 55 personnes inscrites avant le début des journées.
• 3 orateurs invités (Claudia F., Rodolphe L., Guillaume M-M).
• 16 (13+3) exposés/présentations.
• Une moitié des exposés par des thésards
• Laboratoires de provenance:
  • Amérique du Sud (4)
  • IDF (ENSIEE (1), INRIA Paris (2), IRIF (10), LIPN (6), LIX (5), LSV (5), LRI (11), Mines Paritech (1))
  • Lyon: LIP (6)
  • Marseille (1)
  • Nantes (1)
  • Rennes (1)
• Le GDR-IM a fourni une rallonge sur le budget du GT pour l'organisation de ces journées inaugurales.

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.

• Actualisation de la liste des membres;
• Diffusion d'informations sur la mailing-list;
• Identification des équipes qui émergent ou se structurent (p.ex. Galinette) et projets en préparation/maturation (ANR / ERC / PEPS);
• Partage d'informations entre les labo/équipe impliquées dans le GT: postes à l'ouverture, organisation de conférences, invités de long terme, arrivée de post-docs, démarrage de thèses ou soutenances, etc…)
• Remontée de propositions d'informations au GDR (médailles du CNRS, …)
• Structuration scientifique?

• Quand? (premier ou second semestre 2019??)
• Où? (des volontaires?)
• Comment? (1 ou 2 jours? adossé à un autre événement?)