News
Prix de thèse du GDR GPL pour Mickaël Laurent
Mickaël Laurent, ancien doctorant du LMF et de l'IRIF, encadré par Giuseppe Castagna et Kim Nguyễn, a reçu le prix de thèse du GdR Génie de la Programmation et du Logiciel, décerné le 19 juin lors des journées nationales du GdR.
Sa thèse est intitulée Inférence de types polymorphes pour des langages dynamiques : reconstruction de types pour des systèmes combinant polymorphisme paramétrique, surcharge et sous-typage”. Félicitations à Mickaël pour son excellent travail !
(photo avec l'autorisation des personnes, de gauche à droite Anouck Chan, première accessit, Pascal Poizat, co-président du jury et Mickaël)
Plus d'informations sur le site du GdR.
Science flash: Where does time actually come from?
A New Scientist column entitled "Where does time actually come from?" discusses the recent contribution by Pablo Arrighi and Gilles Dowek from LMF and Amélia Durbec from IEMN, to the somewhat fundamental questions about the nature of Time.
Since the laws of Physics are time-reversible, what makes the difference between past and future? Entropy may increase, but how come it was low to begin with? And by-the-way, what happened even before it was at its lowest? And what if... working with toy model graph dynamics, could suggest simple CompSci answers to big Physics questions?
PhD Defense: Luc Chabassier
Aspects of Category Theory in Proof Assistants
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.
Best-Paper Award at ETAPS 2025
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...
PhD Defense: Thomas Soullard
Synthesis for Games of Imperfect Information under Full-Information Protocols
Monday 7 July 2025 at 14h00
ENS Paris-Saclay, Room 1B36 and online
Abstract: Different models can be used to represent programs, to check their correctness, or even better to synthesise them from a specification. Here, we model a program as a player against an environment. Constructing a correct program then boils down to synthesising a winning strategy in the associated game, that is, a behaviour that ensures that the winning condition is satisfied regardless of the behaviour of the environment.
We introduce a new class of games where the player receives imperfect information by communicating with passive observers in a full-information protocol. Unlike the classical model, the player can in one moment obtain an unbounded amount of information.
Séminaire au vert, Port Royal à Saint-Lambert, 2 – 3 juin 2025
The LMF seminar 2025 takes place on June 2-3, 2025 at Centre Port Royal in Saint-Lambert.
Book Release : Learn Programming with OCaml
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.
Rencontre avec les ''Décodeuses du numérique"
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.
PhD Defence: Émilie Grienenberger
Combining computational theories
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...
PhD Defense: Emilie Grienenberger
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