News

Aspects of Category Theory in Proof Assistants

Jul 7 14:00 ₂₀₂₅

Monday 7 July 2025 at 14h00
ENS Paris-Saclay, Room 1B26

Abstract: While the use of proof assistants in mathematical research has yet to become the norm, an increasing number of results have been formalized. The prevalence of category theory in recent mathematical research indicates the need for its formalization in proof assistants. However, category theory is challenging to formalize for reasons we will explore.

The first difficulty is due to the fact that proposition equality in dependently typed theories as a structure that interacts in a complicated way with categories formalised inside those theories. We describe those challenges, and propose some solutions we explored to this problem.

The second difficulty is more pragmatic. One big advantage of category theory is its ability to be reasoned with using graphical languages. However, most proof assistants are text based; thus their notation systems cannot express any graphical language. We implement a plugin to graphically progress category theory proofs in the Coq proof assistant. After a quick demo, we will describe the differents challenges in the implementation of such a software.

Read more...

Patricia Bouyer (LMF, CNRS), B Srivathsan (CMI and ReLaX, India) and Vaishnavi Vishwanath (CMI, India) received the Best ETAPS Paper Award in 2025, which is given to the best theoretical paper at ETAPS, the International Joint Conferences on Theory and Practice of Software. Read more...

Synthesis for Games of Imperfect Information under Full-Information Protocols

Jul 7 14:00 ₂₀₂₅

Lundi 7 juillet 2025 à 14h00
ENS Paris-Saclay, Salle 1B36

Résumé : Différents modèles peuvent être utilisés pour représenter des programmes, pour vérifier s’ils sont corrects, ou mieux pour en synthétiser à partir d’une spécification. Nous modélisons ici un programme par un joueur affrontant un environnement. Construire un programme correct revient alors à synthétiser une stratégie gagnante dans ce jeu, c’est à dire un comportement qui assure de vérifier la condition de victoire quel que soit le comportement de l’environnement.

Nous introduisons un nouveau type de jeu dans lesquels le joueur obtient une information imparfaite en communiquant avec des observateurs passifs, via un full-information protocol. Contrairement au modèle classique on peut obtenir en un instant une quantité non bornée d'information.

Nous proposons une méthode pour synthétiser des stratégies pures et randomisées dans ces jeux, applicable dès qu'un morphisme information-commutant peut être construit.

Read more...

The LMF seminar 2025 takes place on June 2-3, 2025 at Centre Port Royal in Saint-Lambert.

Read more...

Learn Programming with OCaml is a new book by Sylvain Conchon and Jean-Christophe Filliâtre. This is an English translation (by Urmila Nair) of the French edition Apprendre à programmer avec OCaml.

The book is available as a PDF file, under the CC-BY-SA license. The source code for the various programs contained in the book is available for download, under the same license.

The book is structured in two parts. The first part is a tutorial-like introduction to OCaml through 14 small programs, covering many aspects of the language. The second part focuses on fundamental algorithmic concepts, with data structures and algorithms implemented in OCaml.

500 élèves réunis par le CNRS et le Rectorat de Paris ont rencontré les Décodeuses du numérique, des héroïnes de bande dessinée et des scientifiques inspirantes.

À travers des échanges et des ateliers pratiques, cet événement visait à déconstruire les stéréotypes de genre et à ouvrir le champ des possibles pour les filles dans les sciences informatiques.

https://youtu.be/XI1u9UPd21o

Combining computational theories

Feb 3 14:30 ₂₀₂₅

Monday 3 February 2025 at 14h30
ENS Paris-Saclay, Room 1Z14

Abstract. Proof checkers and proof assistants are used to formalize mathematical theorems and verify software, notably critical systems such as medical, industrial and transport systems. The diversity of proof systems raises the question of their interoperability: how can proofs be rechecked and reused across systems? Logical frameworks such as the λΠ-calculus modulo theory provide a common formalism in which various logical systems and mathematical theories can be expressed. The proof transformation tools within the λΠ-calculus modulo theory allow proofs to be translated from one logical system another. In a similar way to logical frameworks, theories combining several theories provide a common language between theories. The main focus of this manuscript is the study of the definition and properties of these theories, specifically in the context of computational theories, that is whose definition relies on rewriting. Read more...

Feb 3 14:30 ₂₀₂₅

Combining computational theories

Monday 3rd February, at 14h30

Room 1Z14

Abstract. Proof checkers and proof assistants are used to formalize mathematical theorems and verify software, notably critical systems such as medical, industrial and transport systems. The diversity of proof systems raises the question of their interoperability: how can proofs be rechecked and reused across systems? Logical frameworks such as the lambdaPi-calculus modulo theory provide a common formalism in which various logical systems and mathematical theories can be expressed. The proof transformation tools within the lambdaPi-calculus modulo theory allow proofs to be translated from one logical system another.

In a similar way to logical frameworks, theories combining several theories provide a common language between theories. The main focus of this thesis is the study of the definition and properties of these theories, specifically in the context of computational theories, that is whose definition relies on rewriting. More specifically, combinations of computational theories will be studied in two contexts: ecumenical logics, i.e. logics that combine intuitionistic and classical logics, and theories of pure type systems modulo rewriting, which are used in the lambdaPi-calculus modulo theory to express logical systems of various proof assistants.

Jury:

• Valeria de Paiva, Topos Institute - Rapportrice
• Cezary Kaliszyk, The University of Melbourne - Rapporteur
• Elaine Pimentel, UCL Computer Science - Examinatrice
• Assia Mahboubi, Inria - Examinatrice
• Jean-Baptiste Joinet, Université Jean Moulin - Examinateur
• Gilles Dowek, Inria - Directeur
• Dale Miller, Inria - Co-encadrant

Chaque année, l'Académie des sciences remet près de quatre-vingt prix couvrant l'ensemble des domaines scientifiques, aussi bien fondamentaux qu'appliqués. Lors de la cérémonie de remise de prix du 26 novembre 2024, Gilles Dowek a reçu la Médaille d'histoire des sciences et d'épistémologie.

Gilles Dowek explore de nouvelles questions philosophiques posées par le développement de l'informatique. Ces questions portent sur le rôle du calcul dans la définition de la vérité mathématique, sur les rapports entre la thèse de Church-Turing et celle de Galilée, selon laquelle l'Univers est écrit en langue mathématique, sur la notion de langage formel et son lien à l'écriture et sur la construction d'une éthique de l'informatique. — Citation du prix

La médaille d’Histoire des sciences et d’épistémologie récompense une ou un scientifique en pleine activité de toute nationalité travaillant dans un laboratoire français de recherche public ou privé ayant contribué par des résultats particulièrement prometteurs au développement de sa discipline, sans restriction sur la nature fondamentale ou appliquée de ses recherches.

Crédit photo : © Académie des sciences – Mathieu Baumer

Each year, the French Academy of Sciences awards nearly eighty prizes covering the entire specrum of fundamental and applied sciences. At the award ceremony of 26 November, 2024, Gilles Dowek was bestowed with the Medal for Contributions to the History and Philosophy of Science.

Gilles Dowek explores new philosophical questions raised by the development of computer science. These questions address the role of computation in defining mathematical truth, the relationship between the Church-Turing thesis and Galileo's principle that the Universe is written in the language of mathematics, the concept of formal languages and their connection to writing, and the construction of an ethics of computer science.

— Award citation

The Medal for Contributions to the History and Philosophy of Science is awarded to an active scientist of any nationality working in a French public or private research laboratory who has contributed particularly promising results to the development of their discipline, without restriction on the fundamental or applied nature of their research.

Photo credit: © Académie des sciences – Mathieu Baumer