L’atelier sera axé sur la recherche en calculs computationnels. Ceux-ci doivent être compris au sens large comme englobant les cadres logiques, les langages de programmation et les théories des types.
Idéalement, l’étude et le développement des calculs computationnels devraient être entrepris de manière bidirectionnelle, à partir des perspectives complémentaires de leur modélisation sémantique et de leur formalisation syntaxique. Ces deux aspects peuvent être abordés de manière quelque peu indépendante et font en effet l’objet de contributions importantes au sein de divers groupes de recherche. Le développement et l’exploitation de l’interface entre eux sont extrêmement fructueux et offrent des opportunités prometteuses pour la recherche. L’atelier stimulera ce type de pollinisation croisée en réunissant des chercheurs travaillant sur des modèles mathématiques et des chercheurs travaillant sur la formalisation/mise en œuvre informatique, les deux perspectives étant représentées de manière égale, afin de favoriser de nouvelles recherches.
L’atelier se concentrera sur l’examen des défis de recherche dans ce domaine, parmi lesquels nous avons actuellement identifié les suivants :
− L’automatisation de la métathéorie prouvée correcte pour les calculs de types dépendants à partir de modèles mathématiques.
− L’extraction de code informatique réellement exécutable à partir de preuves mathématiques formalisées.
− L’utilisation pratique et le calcul avec des quotients dans les preuves mécanisées.
− La formalisation d’une structure algébrique cohérente de dimension supérieure dans les assistants de preuve.
− L’extension modulaire des théories des types dépendants (intégrant en particulier la linéarité, les effets computationnels et/ou les modalités) et leurs applications.