News & Events
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: Louis Lemonnier
The Semantics of Effects: Centrality, Quantum Control, and Reversible Recursion
Mercredi 19 juin 2024 à 14h
ENS Paris-Saclay, Amphithéâtre Lagrange, salle 1Z14 and online.
My manuscript is available here.
Résumé. Le sujet de cette thèse est axé sur la théorie des langages de programmation. Dans un langage de programmation suffisamment bien défini, le comportement des programmes peut être étudié à l'aide d'outils empruntés à la logique et aux mathématiques, énonçant des résultats sans exécuter le code.
Ce domaine de l'informatique est appelé "sémantique". La sémantique d'un langage peut se présenter sous plusieurs formes : dans notre cas, des sémantiques opérationnelles, des théories équationnelles et des sémantiques dénotationnelles. 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.
Prix de thèse du GdR GPL pour Xavier Denis
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.
Séminaire au vert, Saint-Rémy-lès-Chevreuse, 13 – 14 juin 2024
The LMF seminar 2024 took place on June 13–14, 2024 at Domaine Saint-Paul in Saint-Rémy-lès-Chevreuse.
MT180s : Gaspard Fougea reçoit le prix du jury à la finale Université Paris-Saclay
Toutes nos félicitations à Gaspard Fougea pour le prix du jury reçu à la finale Université Paris-Saclay du concours Ma thèse en 180 secondes.
Gaspard prépare sa thèse « Modèles formels pour la conscience : de l’expérience subjective aux algorithmes cognitifs » au LMF sous la direction d'Alain Finkel et Stéphane le Roux.
Soutenance de thèse : Olivier Stietel
Local First Order Logic with Data: Toward Specification of Distributed Algorithms
Jeudi, 14 décembre 2023, 14h00
Université Paris CIté, Bâtiment Sophie Germain, salle 3052
Soutenance de thèse : Antoine Lanco
Stratégies pour la réduction forte
Vendredi 15 décembre 2023 14h
Université Paris-Saclay, bâtiment 660 (amphithéâtre) et visioconférence
Résumé: La sémantique d’un langage de programmation, et d’un langage fonctionnel en particulier, laisse généralement une certaine liberté quant à l’ordre dans lequel sont effectuées les différentes opérations. Les différentes stratégies qui peuvent être adoptées, comme l'appel par valeur ou l'évaluation paresseuse, bénéficient déjà à la fois d'un large corpus théorique et de nombreuses implémentations efficaces. Ce corpus cependant est majoritairement tourné vers un objectif d'évaluation des programmes, c'est-à-dire de production d'une valeur. Le cadre associé est celui de l'évaluation faible, dans lequel aucune évaluation n'est effectuée à l'intérieur d'une fonction qui ne serait pas totalement appliquée. En effet, dans un langage fonctionnel la fermeture représentant une telle fonction est déjà en elle-même considérée comme une valeur. Read more...
Soutenance de thèse : Alexandrina Korneva
The Cubicle Fuzzy Loop: A Testing Framework for Cubicle
Vendredi 8 décembre 2023 10h30
Université Paris-Saclay, bâtiment 650, salle 435 (salle des thèses)
Résumé. L’objectif de cette thèse est d’intégrer une technique de test dans le model checker Cubicle. Pour cela, nous avons étendu Cubicle avec une boucle de Fuzzing (appelée Cubicle Fuzzy Loop – CFL). Cette nouvelle fonctionnalité remplit deux fonctions principales. Tout d’abord, elle sert d’oracle pour l’algorithme de génération d’invariants de Cubicle. Ce dernier, basé sur une exploration en avant de l’ensemble des états atteignables, était fortement limité par ses heuristiques lorsqu’elles sont appliquées à des modèles fortement concurrents. Read more...
Soutenance de thèse : Nathan Thomasset
Stratégies à mémoire finie dans les jeux concurrents à deux joueurs.
Jeudi 21 décembre 2023 à 14h00
ENS Paris-Saclay, Salle 1Z71, zoom
Résumé. On étudie des jeux concurrents à deux joueurs de durée infinie qui se jouent de la façon suivante : chaque tour, les deux joueurs choisissent chacun une action sans connaître le choix actuel de l'adversaire. Sur un nombre de tours infini, cette procédure génère une suite infinie de paires d'actions. Cette suite est alors gagnante pour le Joueur 1 si elle appartient à l'ensemble gagnant du jeu. Read more...
PhD Defence: Giann Karlo
Ecosystem causal analysis using Petri net unfoldings
by Giann Karlo
Thursday 14 December 2023 at 9 am
ENS Paris-Saclay, Room 1Z53 and Zoom
Abstract. Many verification problems for concurrent systems have been successfully addressed by various methods over the years, particularly Petri net unfoldings. However, questions of long-term behavior and stabilization have received relatively little attention. For instance, crucial features of the long-term dynamics of ecosystems, such as basins of attraction and tipping points, remain difficult to identify and quantify with good coverage. Read more...
PhD Defence: Xavier Denis
Deductive Verification of Rust Programs
by Xavier Denis
Monday 18 December 2023 at 2pm
Batiment 660, Amphitheatre and video conferencing Zoom link.
Abstract. Rust is a programming language introduced in 2015, which provides the programmer with safety features regarding the use of memory. The goal of this thesis is the development of a deductive verification tool for the Rust language, by leveraging the specificities of its type system, in order to simplify memory aliasing management, among other things. Read more...