CONFERENCE
Synthetic mathematics, logic-affine computation and efficient proof systems
Mathématiques synthétiques, calcul logique affine et systèmes de preuve efficients
8 – 12 September, 2025
Scientific Committee
Comité scientifique
Andrej Bauer (University of Ljubljana)
Olivia Caramello (IHES)
Maria Emilia Maietti (Universita degli Studi di Padova)
Michael Rathjen (University of Leeds)
Organizing Committee
Comité d’organisation
Ingo Blechschmidt (University of Augsburg)
Liron Cohen (Ben-Gurion University of the Negev)
Thierry Coquand (University of Gothenburg)
Sara Negri (University of Genoa)
Peter Schuster (University of Verona)
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.
SPEAKERS
Mohamed Barakat (University of Siegen) CAP — a categorical (re)organization of computer algebra
Ulrik Buchholtz (University of Nottingham) Towards synthetic locale theory
Gabriele Buriola (University of Verona) A constructive picture of Noetherian conditions and well quasi-orders
El Mehdi Cherradi (IRIF Paris) Internal languages of locally cartesian closed (∞,1)-categories
Felix Cherubini (Chalmers University of Technology) The abelian closure of finite free modules in synthetic algebraic geometry
Tom De Jong (University of Nottingham) Formalizing equivalences without tears
Sophie D’Espalungue (IRIF) Towards an internal construction of meaning
Jacopo Emmenegger (University of Genova) Towards the effective 2-topos
Laura Fontanella (Université Paris Est Créteil) Realizability models for set theory
Yannick Forster (Inria Paris) Recent advances on synthetic computability and infinity
Jonas Frey (Université Sorbonne Paris Nord) Modest sets and equilogical spaces as mono-fibrational cocompletions
Jacopo Furlan (Université Paris 13) Bar induction and preservation of cardinals
Luis Gambarte (Ludwig-Maximilians-University Munich) Equivalences between categories with dependent arrows and comprehension categories
Freek Geerligs (University of Gothenburg) Synthetic Stone duality
Hugo Herbelin (INRIA, Rocquencourt-Paris) Cubical models of parametric type theory in indexed form
Joost Joosten (Universitat de Barcelona) Efficient proof systems in provability logics
Ryota Kuroki (University of Tokyo) A quantitative Hilbert’s basis theorem and the constructive Krull dimension
Maria Emilia Maietti (University of Padova) A geometric property of localic and realizability toposes
Etienne Miquey (Aix-Marseille Université) Generic approaches to effectful realizability
Hugo Moeneclaey (University of Gothenburg) From synthetic Stone duality to synthetic algebraic topology
Ming Ng (Nagoya University) What is a space, and why should a logician care?
Pierre-Marie Pédrot (INRIA) Implying implications can go another direction
Iosif Petrakis (University of Verona) Orthocomplemented subspaces and partial projections on a Hilbert space
Emily Riehl (Johns Hopkins University) Synthetic perspectives on the Yoneda lemma
Quentin Schroeder (Université Paris 13) Mnemetic monads and compactness
Alex Simpson (University of Ljubljana) Synthesising random variables
Benno Van Den Berg (University of Amsterdam) Constructive ordinals
Jonathan Weinberger (Chapman University) Universes in synthetic (∞,1)-category theory
SPONSORS
