News & Events

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

It also happens online: connection link.

Résumé (in French, English version below)

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. Les premières donnent un sens opérationnel aux programmes, au sein de la syntaxe du langage. Elles simulent les opérations qu'un ordinateur est censé effectuer s'il exécute le programme. Une théorie équationnelle fonctionne également de manière syntaxique : elle indique si deux programmes effectuent la même opération sans informer sur la procédure. Enfin, la sémantique dénotationnelle est l'étude mathématique des programmes, généralement à l'aide de la théorie des catégories. Elle permet par exemple de prouver qu'un programme se termine ou non.

Cette thèse se concentre sur la sémantique des effets dans les langages de programmation – une fonctionnalité ajoutée à un langage, gérant des données secondaires ou des résultats probabilistes. Eugenio Moggi, en 1991, a publié un travail fondateur sur l'étude de la sémantique des effets, soulignant la relation avec les monades en théorie des catégories. La première contribution de cette thèse suit directement le travail de Moggi, en étudiant la commutativité des effets dans un langage de programmation à travers le prisme des monades. Les monades sont la généralisation de structures algébriques telles que les monoïdes, qui ont une notion de centre : le centre d'un monoïde est une collection d'éléments qui commutent avec tous les autres dans le monoïde. Nous fournissons les conditions nécessaires et suffisantes pour qu'une monade ait un centre. Nous détaillons également la sémantique d'un langage de programmation avec des effets qui portent des informations sur les effets qui sont centraux. De plus, nous fournissons un lien fort – un résultat de langage interne – entre ses théories équationnelles et sa sémantique dénotationnelle.

Le deuxième axe de la thèse est l'informatique quantique, perçue comme un effet réversible. Le quantique est un domaine émergent de l'informatique qui utilise la puissance de la mécanique quantique pour calculer. Au niveau des langages de programmation, de nouveaux paradigmes doivent être développés pour être fidèles aux opérations quantiques. Les opérations quantiques physiquement permises sont toutes réversibles, à l'exception de la mesure ; cependant, la mesure peut être reportée à la fin du calcul, ce qui nous permet de nous concentrer d'abord sur la partie réversible et d'appliquer ensuite la mesure pour obtenir des résultats. Dans le chapitre correspondant, nous définissons un langage de programmation réversible, avec types simples, qui effectue des opérations quantiques "unitaires". Une sémantique dénotationnelle et une théorie équationnelle adaptées au langage sont présentées, et nous prouvons que cette dernière est complète. Ce travail vise à fournir des bases solides pour l'étude du contrôle quantique d'ordre supérieur. En outre, nous étudions la récursion réversible, en fournissant une sémantique opérationnelle et dénotationnelle adéquate à un langage de programmation fonctionnel, réversible et Turing-complet. La sémantique dénotationnelle utilise l'enrichissement dcpo des catégories inverses. Ce modèle mathématique sur l'informatique réversible ne se généralise pas directement à sa version quantique. Dans la conclusion, nous détaillons les limites et l'avenir possible du contrôle quantique d'ordre supérieur.

Membres du jury :

  • Thomas Ehrhard, Directeur de recherche, CNRS - Rapporteur & Examinateur
  • Claudia Faggian, Chargée de recherche, CNRS - Examinatrice
  • Jean Goubault-Larrecq, Professeur des universités, ENS Paris-Saclay - Examinateur
  • Marie Kerjean, Chargée de recherche, CNRS - Examinatrice
  • Laurent Regnier, Professeur des universités, Aix-Marseille Université - Rapporteur & Examinateur

Équipe d'encadrement :

  • Pablo Arrighi, Professeur des universités, Université Paris-Saclay - Directeur de thèse
  • Benoît Valiron, Maître de conférence, CentraleSupélec - Co-encadrant de thèse
  • Vladimir Zamdzhiev, Chercheur, Inria - Co-encadrant de thèse

Abstract

The topic of this thesis revolves around the theory of programming languages. In a sufficiently well-defined programming language, the behaviour of programs can be studied with tools borrowed from logic and mathematics, allowing us to state results without executing the code. This area of computer science is called “semantics”. The semantics of a programming language can take several forms: in this thesis, we work with operational semantics, equational theories, and denotational semantics. The former gives an operational meaning to programs but within the language’s syntax. It simulates the operations a computer is supposed to perform if it were running the program. An equational theory also works syntactically: it indicates whether two programs perform the same operation without giving any information on the procedure. Lastly, denotational semantics is the mathematical study of programs, usually done with the help of category theory. For example, it allows us to prove whether a program terminates.

This thesis focuses on the semantics of effects in programming languages – namely, a feature added to a language, e.g. handling side data or probabilistic outputs. Eugenio Moggi, in 1991, published foundational work on the study of the semantics of effects, highlighting the relationship with monads in category theory. The first contribution of this thesis directly follows Moggi’s work, studying the commutativity of effects in a programming language through the prism of monads. Monads are the generalisation of algebraic structures such as monoids, which have a notion of centre: the centre of a monoid is a collection of elements which commute with all others in the monoid. We provide the necessary and sufficient conditions for a monad to have a centre. We also detail the semantics of a programming language with effects that carry information on which effects are central. Moreover, we provide a strong link – an internal language result – between its equational theories and its denotational semantics.

The second focus of the thesis is quantum computing, which is seen as a reversible effect. Quantum computing is an emergent field in computer science that uses the power of quantum mechanics to compute. At the level of programming languages, new paradigms need to be developed to be faithful to quantum operations. Physically permissible quantum operations are all reversible, except measurement; however, measurement can be deferred at the end of the computation, allowing us to focus on the reversible part first and then apply measurement to obtain results. In the corresponding chapter, we define a simply-typed reversible programming language performing quantum operations called “unitaries”. A denotational semantics and an equational theory adapted to the language are presented, and we prove that the latter is complete. The aim of this work is to provide a solid foundation for the study of higher-order quantum control. Furthermore, we study recursion in reversible programming, providing adequate operational and denotational semantics to a Turing-complete, reversible, functional programming language. The denotational semantics uses the dcpo enrichment of rig join inverse categories. This mathematical account of higher-order reasoning on reversible computing does not directly generalise to its quantum counterpart. In the conclusion, we detail the limitations and possible future for higher-order quantum control.

Séminaire au vert, Saint-Rémy-lès-Chevreuse, 13 – 14 juin 2024

The LMF seminar 2024 will occur on June 13–14, 2024 at Domaine Saint-Paul in Saint-Rémy-lès-Chevreuse.

Read more...

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.

https://www.youtube.com/watch?v=SYZ5LvZieOA

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

Read more...

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

Giann Karlo

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...

Best-Paper Award at JELIA 2023

Stéphane Demri (LMF, CNRS) and Karin Quaas (Leipzig University) received the Best-Paper Award at JELIA 2023, the 18th Edition of the European Conference on Logics in Artificial Intelligence, which is a major forum for logic-based approaches to AI. Read more...