News & Events

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

Formal Proofs in Applied Mathematics: A Coq Formalization of Simplicial Lagrange Finite Elements

Dec 9 14:00 ₂₀₂₄

Monday 9 December 2024 at 14h00
ENS Paris-Saclay, Room 1B26

Abstract. This thesis is dedicated to developing formal proofs of mathematical theorems and propositions within the field of real analysis using the Coq proof assistant to ensure their correctness. The core of this work is divided into two main parts. The first part focuses on using Coq to formalize key mathematical principles such as the Lebesgue induction principle and the Tonelli theorem, allowing the computation of double integrals on product spaces by iteratively integrating with respect to each variable. This work builds upon previous research in measure theory and the Lebesgue integral. The second part of this thesis operates within the framework of the Finite Element Method (FEM), a widely used numerical technique for solving partial differential equations (PDEs). Read more...

Exécution symbolique pour tous ou Compilation d’OCaml vers WebAssembly

Dec 16 14:00 ₂₀₂₄

Lundi 16 décembre 2024 à 14h
Amphithéâtre du bâtiment 660, Avenue des Sciences, 91190 Gif-sur-Yvette

Résumé. Les limitations de JavaScript en tant que langage par défaut du Web ont conduit au développement de WebAssembly (Wasm), un langage sûr, efficace et modulaire. Toutefois, compiler des langages à glaneur de cellules vers Wasm ne se fait pas sans peine, notamment du fait de la nécessité de réécrire le moteur d’exécution ou de la gestion des interactions avec le glaneur de cellules de l’hôte (le navigateur). Des extensions, dont WasmGC, ont été développées par les groupes de travail Wasm pour faciliter cette tâche. Nous présentons Wasocaml, le premier compilateur d’OCaml vers WasmGC. Ce projet confirme l’adéquation de la proposition WasmGC pour des langages fonctionnels et a influencé son développement. Les stratégies de compilation mises en œuvre dans Wasocaml peuvent également être appliquées à d’autres compilateurs et langages ; deux compilateurs les ont d’ailleurs déjà adoptées.Read more...

We are delighted to announce that two researchers with strong ties to our laboratory have won the Ackermann Award 2024:

🌟 Gaëtan Douéneau-Tabot

A former student at ENS Paris-Saclay, Gaëtan was recognised for his thesis, Optimization of String Transducers, supervised by Olivier Carton (IRIF, Université Paris-Cité) and Emmanuel Filiot (Université Libre de Bruxelles).

🌟 Aliaume Lopez

Aliaume completed a joint PhD between LMF and IRIF (Université Paris-Cité). His award-winning thesis, First Order Preservation Theorems in Finite Model Theory: Locality, Topology, and Limit Constructions, was supervised by Jean Goubault-Larrecq (LMF) and Sylvain Schmitz (IRIF, Université Paris-Cité).

The Ackermann Award is the Outstanding Dissertation Award for Logic in Computer Science, presented annually by the the European Association for Computer Science Logic (EACSL) during the Computer Science Logic (CSL) conference.

This year’s achievements continue a proud tradition in our laboratory, following in the footsteps of previous Ackermann Award recipients, Marie Fortin (2021) and Amina Doumane (2018).

Nov 8 9:00 ₂₀₂₄

Le LMF et le DER Informatique de l'ENS Paris-Saclay organisent un workshop le vendredi 8 novembre 2024, à l'occasion du départ à la retraite de Serge Haddad. Il aura lieu dans les locaux de l'ENS Paris-Saclay.

La participation est gratuite, mais pour des raisons de logistique, il est demandé de vous inscrire.

Programme

9h30 – 9h45 Accueil, café (Simondon)

9h45 – 10h Introduction de la journée (Simondon 1B36)

10h – 12h15 Serge & certains de ses collaborateurs (Simondon 1B36)

• 10h - 10h45 : Béatrice Bérard (LIP6) - The story of Interrupt Timed Automata
• 10h45 - 11h30 : Susanna Donatelli (Universita' di Torino)
• 11h30 - 12h15 : Didier Lime (LS2N), Olivier Roux (LS2N)

12h15 – 14h00 Déjeuner (Espace Kafé)

14h00 – 15h30 Serge & certains de ses anciens doctorants, également anciens élèves de l'ENS Cachan (Simondon 1B36)

• 14h-14h30 : Benoit Barbot (LACL) - Importance Sampling. When Statistical Verification Meets Numerical Verification
• 14h30-15h : Yann Duplouy (LMF) - Modélisation de systèmes hybrides probabilistes : Cosmos et Simulink
• 15h-15h30 : Engel Lefaucheux (LORIA) - Diagnosis of probabilistic systems: Cheaper, better, faster, stronger

15h30 – 16h15 Serge & le projet Mefosyloma (Simondon 1B36)

• 15h30-16h15 : Fabrice Kordon (LIP6), Laure Petrucci (LIPN) - Serge unveiled

16h15 Cocktail (Espace Kafé)

Distributed Bacterial Circuit Design

Oct 1 10:00 ₂₀₂₄

Tuesday, 1 October 2024 at 10:00am

ENS Paris-Saclay, room 1B26

Abstract. Biological circuits often suffer from high noise and high cellular burden that can lead to cell death. In this thesis, we explore distributed biological circuit design to present solutions for biological computations in high-noise environments. We first designed a new language oriented to the distributed circuit design, solving the limitations of previously existing tools. Secondly, we presented a distributed algorithm for distributed biological circuits that coordinates a population of cells to find an analyte of interest resistant to noise. The algorithm is more sensitive than the state-of-the-art individual cell algorithms. Finally, we provide a new algorithm to validate the previous algorithm using quasi-stationary distributions in a stochastic model instead of our initially used deterministic ordinary differential equation model.

Read more...

On Quantum Programming Languages

Sep 24 10:00 ₂₀₂₄

Tuesday 24 September 2024, at 10h

Salle des Thèses, Bâtiment 650 Ada Lovelace

The event will be held in a hybrid format.

Abstract

This thesis—Habilitation à diriger des recherches—presents some of my research contributions since my Ph.D defense in 2008. I have had the chance to participate in the development of quantum programming languages since their early developments: the presentation aims to present my point of view on the evolution of the subject, my contributions, and the current research trends in the community. The target audience is a graduate student interested in pointers to the field of quantum programming languages.

Read more...

Generic Bidirectional Typing in a Logical Framework for Dependent Type Theories

Sep 18 15:00 ₂₀₂₄

Wednesday 18 September 2024, at 15h

ENS Paris-Saclay, room 1Z18, Zoom link

The current version of the manuscript can be found here.

Abstract.

Dependent type theories are formal systems that can be used both as programming languages and for the formalization of mathematics, and constitute the foundation of popular proof assistants such as Coq and Agda. In order to unify their study, Logical Frameworks (LFs) provide a unified meta-language for defining such theories in which various universal notions are built in by default and metatheorems can be proven in a theory-independent way. Read more...

Prétraitement compositionnel en Coq

Jul 10 14:00 ₂₀₂₄

Mercredi 10 juillet 2024 à 14h

ÉNS Paris-Saclay, salle 1Z31, Lien Zoom.

Abstract. This thesis presents a new methodology for preprocessing goals in the Coq proof assistant in order to send them to an automatic solver. This methodology consists of composing atomic and certifying transformations based on the goal to be proven. We will first present the library of transformations that we have written, then we will present an orchestrating tool for these transformations, which aims to be generic. This has led to the implementation of a new 'push-button' tactic called 'snipe' for Coq.

Read more...

An Ontology Framework for Formal Libraries

Jul 12 13:30 ₂₀₂₄

Vendredi 12 juillet 2024 à 13:30h, Batiment 650, 435 (Salle des Theses).

Abstract.

Document ontologies, i. e., a machine-readable form of the structure of documents as well as the document discourse, play a key role in structuring the link between semantic notions and documents containing infor- mal text. In many scientific disciplines such as medicine or biology, ontologies allows the organization of research papers and their automated access. There are particular challenges in the field mathematics and engineering where documents contain both formal and informal text- elements with a complex structure of mutual links and dependencies of various types. Texts may contain formulas (which should be at least type-correct and if possible semantically consistent with the formal definitions) and formal definitions based on naming conventions that should reflect informal explanations. A deeper access into the formal parts of this type of documents involves a framework that can cope with typed, logical languages, which requires going substantially further than existing ontological languages like, for example, OWL.

Read more...

Measuring Well Quasi-Orders and Complexity of Verification

Jul 3 14:00 ₂₀₂₄

Mercredi 3 juillet 2024 à 14h

ENS Paris-Saclay, salle 1Z18, Lien Zoom.

Abstract. We investigate three ordinal measures of a well quasi-order, also called ordinal invariants: maximal order type, width, and height. One main challenge is to compute the ordinal invariants of complex well quasi-orders built from simpler well quasi-orders through classical operation, such as the Cartesian product, and high-order constructions, like the finite words embedding.

In this thesis, we compute compositionally the maximal order type of the direct product, the width of the multiset embedding, and the height and width of the multiset ordering. Furthermore, we compute the width of the Cartesian product in restricted cases and prove tight bounds on the ordinal measures of the finite powerset. Read more...

Jun 21 9:30 ₂₀₂₄

Title: Polymorphic type inference for dynamic languages: reconstructing types for systems combining parametric, ad-hoc, and subtyping polymorphism

Friday, June 21th at 09:30 (Paris time, UTC+2)
Batiment Sophie Germain, 3rd floor, Room 3052 8 Pl. Aurélie Nemours, 75013 Paris

Zoom link: https://u-paris.zoom.us/j/83379216296?pwd=ZxYiEqpCprbs9leonLXgEbniPVmwXs.1 Meeting ID: 833 7921 6296 Passcode: 341938

Abstract. Programming languages can be broadly categorized into two groups: static languages, such as C, Rust, and OCaml, and dynamic languages, such as Python, JavaScript, and Elixir. While static languages generally offer better performance and more security thanks to a phase of static typing that precedes compilation ("well-typed programs cannot go wrong"), this often comes at the expense of flexibility, making programs safer but prototyping more tedious. In this defence, I present a formal system for statically typing dynamic languages, offering a compromise between safety and flexibility.

Read more...

Xavier Denis, ancien doctorant du LMF, encadré par Jacques-Henri Jourdan et Claude Marché, a reçu le prix de thèse du GdR Génie de la Programmation et Logiciel, décerné mardi 5 juin lors des journées nationales du GdR.

Sa thèse est intitulée Deductive Verification for Rust Programs. Félicitations à Xavier pour son excellent travail !

Plus d'informations sur le site du GdR.