Synthetic frameworks have proved to be pivotal tools at the interface of mathematics and informatics, especially enabling concise formalizations and custom proof systems. Noteworthy achievements include homotopy type theory, synthetic computability theory, and synthetic algebraic geometry. Very similar paradigms characterize the related areas of logic-driven computational algebra and geometry, sheaf models and modern realizability theory, and strong negation for constructive reasoning with negative information. Contrasting yet complementary approaches are about to converge, emphasizing the imperative of unifying theoretical underpinnings with practical implementation. With the proposed seminar we aim to extend and deepen the convergence across disciplinary boundaries by fostering exchange and collaboration among experts and practitioners.

Les cadres synthétiques se sont révélés être des outils essentiels à l’interface des mathématiques et de l’informatique, permettant notamment des formalisations concises et des systèmes de preuve sur mesure. Les réalisations remarquables incluent la théorie homotopique des types, la théorie synthétique de la calculabilité et la géométrie algébrique synthétique. Des paradigmes très similaires caractérisent les domaines connexes de l’algèbre et de la géométrie computationnelles, guidées par la logique, les modèles de faisceaux et la théorie moderne de la réalisabilité, ainsi que la négation forte pour raisonner de manière constructive avec des informations négatives. Des approches opposées mais complémentaires sont sur le point de converger, soulignant l’impératif d’unifier les bases théoriques avec une implémentation pratique. Avec le séminaire proposé, nous visons à étendre et approfondir la convergence à travers les frontières disciplinaires en favorisant l’échange d’idées et la collaboration entre experts et praticiens.