I am a currently working at the University of Le Havre as a "scientific mediator" for Artificial Intelligence, in the NORMANTHIIA project. In practice, this means that I'm giving non-technical courses about artificial intelligence (machine learning and symbolic approaches) to students that do not study specifically computer science, as well as formations for professors mainly about generative artificial intelligence. I am also acting as a coordinator of a working group on artificial intelligence in the University.
I am taking a break on research, but I am still very interested by type systems, complexity, logic and programming languages, especially in presence of effects (probabilities, concurrency...). Recently, I have also been particularly interested in algebraic effects and handlers, as well as bayesian programming, automatic differentiation and theory of machine learning in general.
You can find the pdf of my PhD Thesis here
Abstract:
Complexity is an important notion in computer science, both for the study of programs and theoretical problems. For a program or an algorithm, complexity corresponds to the amount of resources it needs to compute its output on a given input, indicating information about the efficiency. In practice, two resources are mainly studied: time and space. The static study of this is called complexity analysis. As for problems, the focus is on the study of complexity classes, where problems are regrouped depending on the complexity of the best program that can solve this problem. In this thesis, we study methods based on sized type systems for time complexity, especially for the analysis of processes in the pi-calculus, considered as a communication-based model for parallel computation. The main idea of sized types is to track the size of values in a program, and to use this information to control recursion and deduce time complexity bounds.
In the first part of this thesis, we focus on a theoretical approach of complexity, following the lines of implicit computational complexity (ICC). The goal of ICC is to characterize complexity classes by means of logics or types, generally without explicit bounds. This allows in particular for a deeper understanding of complexity classes. Several methods have been proposed to characterize time complexity classes. One approach comes from linear logic and restricted versions of its !-modality controlling duplication. The first instance of this is light linear logic for polynomial time computation. Another approach, illustrated by non-size increasing types or the sized types defined before, is to focus on the sizes of values. However, both approaches suffer from limitations. The first one has a limited intensional expressivity, that is to say some natural polynomial time programs are not typable. Concerning the second approach, it is essentially linear, more precisely it does not allow for a non-linear use of higher-order arguments. In this thesis, we incorporate both approaches into a common type system, to overcome their respective constraints. The source language we consider is a lambda-calculus with data-types and iteration, a variant of Gödel's system T. We design a type system for this language allowing non-linear functional arguments, with a seemingly good intensional expressivity. Our approach relies on elementary linear logic (ELL), combined with a system of linear sized types. We discuss the expressivity of this new type system, called sEAL, and prove that it gives a characterization of the complexity classes FPTIME and 2k-FEXPTIME.
In the second part of this thesis, we study complexity analysis with types. Type systems as a technique to analyse programs have been extensively studied, especially for functional programming languages where composition is essential. Among all the approaches for this, we focus on sized types. We explore how to extend those types to the analysis of parallel complexity in the pi-calculus. Two notions of time complexity are studied: the total computation time without parallelism (work) and the computation time under maximal parallelism (span). We define operational semantics to capture those two notions. The semantics for span is particularly important, as it allows for simpler proof methods than related notions. We present then two similar type systems from which one can extract a complexity bound on a process, inspired both by sized types and input/output types, with additional temporal information about communications. However, this extension of functional sized types for span analysis has limited expressivity, especially in presence of concurrent behaviours such as semaphores. Aiming for a more expressive analysis, we design a type system which builds on the concepts of usages, originally used for deadlock-freedom analysis.
Email: (λXY.ghyselenYalexisXgmailYcom) @ .
Resume: Contact me !