News & Events
Workshop pour célébrer Serge Haddad, à l'occasion de son départ à la retraite
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é)
PhD Defence: Fabricio Cravo
Distributed Bacterial Circuit Design
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.
HDR defense: Benoît Valiron
On Quantum Programming Languages
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.
Two former students win Ackermann Award 2024
We are delighted to announce that two researchers with strong ties to our laboratory have won the Ackermann Award 2024:
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 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).
Workshop pour célébrer Serge Haddad, à l'occasion de son départ à la retraite
Le LMF et le DER Informatique de l'ENS Paris-Saclay organisent un workshop à l'occasion du départ à la retraite de Serge Haddad le vendredi 8 novembre 2024. Il se tiendra dans les locaux de l'ENS Paris-Saclay.
Pour plus d'informations sur le programme et les modalités d'inscription, veuillez consulter la page du workshop.
Workshop in Honour of Serge Haddad
A special workshop in honour of Serge Haddad on the occasion of his retirement will be held on Friday 8 November 2024 at ENS Paris-Saclay. The event is organised jointly by LMF and the Computer-Science Department of ENS Paris-Saclay.
For information on the programme and registration, visit the workshop page.
ACTS 2023 - Workshop on Automata, Concurrency, and Timed Systems
The 6th edition of the Workshop on Automata, Concurrency, and Timed Systems takes place from 30 May to 2 June 2023 at ENS Paris-Saclay.
The workshop series emerged from a long-standing Indo-French cooperation in the areas of ACTS: Automata and Logic, Concurrency Theory, and Timed Systems. As a special event, this year's programme features a session in honour of Paul Gastin on the occasion of his retirement.
E. W. Beth Dissertation Prize for Aliaume Lopez
Aliaume Lopez received the 2024 E. W. Beth Dissertation Prize for his thesis First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions.
The prize, named in honor of the Dutch mathematician Evert Willem Beth, was established in 1998 by the Association for Logic, Language, and Information (FoLLI) and is awarded annually for outstanding dissertations in the fields of Logic, Language, and Information.
Aliaume prepared his thesis under the joint supervision of Jean Goubault-Larrecq at LSV, then LMF, and of Sylvain Schmitz at IRIF.
PhD Defence: Thiago Felicissimo
Generic Bidirectional Typing in a Logical Framework for Dependent Type Theories
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...
PhD Defence: Louise Dubois de Prisque
Prétraitement compositionnel en Coq
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.
PhD Defence: Nicolas Meric
An Ontology Framework for Formal Libraries
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.
PhD Defence: Isa Vialard
Measuring Well Quasi-Orders and Complexity of Verification
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...
PhD defence of Mickael Laurent
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.