WORKSHOP

Scalp Working Group Days
Journées du GT Scalp (Structures formelles pour le CALcul et les Preuves)

15 – 17 February, 2023

Organizing Committee
Comité d’organisation

Pierre Clairambault (CNRS et Aix-Marseille Université)

   This is the fourth occurrence of the GT Scalp days, the annual meeting organized by the working group Scalp (“Structures formelles pour le Calcul et les Preuves” – Formal Structures for Computation and Proofs). Scalp is a working group of the GDR IM, the CNRS structure federating research in mathematical aspects of computer science in France.
   The GT Scalp animates the French community of researchers working on the mathematical structures behind proofs and programs; with a focus (but not exclusively) on the interface between them. The themes covered by Scalp span an array of disciplines ranging from proof theory to the theory of programming  languages. It covers logic or algebraic calculi (λ-calculi, term or graph rewriting, process calculi. . . ), deduction systems (classical, intuitionistic, linear. . . ), type theory and inference systems, as well as automated or interactive proof systems, with applications to analysis and verification of programs (abstract interpretation, program logics, tree automata. . . ), of their quantitative properties (complexity analysis, probabilistic or quantum program analysis, implicit algorithmic complexity). The methods used can be syntactic (sequent systems, type systems, abstract machines, induction and co-induction, proof search. . . ) or semantic (categories, domains, games, vector spaces, realizability. . . ).
   The objective of the GT Scalp days is to let the community meet and exchange recent ideas or developments. It is of particular importance for young researchers, for whom it is often one of the first opportunities to meet the French community on their research topic.

   Cette rencontre est la quatrième occurrence des Journées du GT Scalp, la rencontre annuelle organisée par le Groupe de Travail Scalp (Structures formelles pour le Calcul et les Preuves) du groupement de recherche (GDR) Informatique Mathématique du CNRS.
   Le GT Scalp anime 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é).
   Les journées du GT ont pour objectif de permettre à la communauté de se rencontrer et de partager idées et résultats récents. Elles permettent en particulier aux jeunes chercheuses et jeunes chercheurs de recontrer, souvent pour la première fois, la communauté française autour de leur thématique de recherche.

SPONSORS

BQR pôle calcul
R. Crubillé
DYVERSE
PPS
RECIPROG