I am a currently a post-doc in the DIAPASoN project at the University of Bologna.

My main research interest are on types, complexity, logic and programming languages, especially in presence of effects (probabilities, concurrency...).

- Publications: see DBLP
- Recent Publications:
- Patrick Baillot and Alexis Ghyselen, CSL 2018, Combining Linear Logic and Size Types for Implicit Complexity .
- Martin Avanzini, Ugo Dal Lago and Alexis Ghyselen, LICS 2019, Type-Based Complexity Analysis of Probabilistic Functional Programs .
- Patrick Baillot and Alexis Ghyselen, TCS 2020 Combining Linear Logic and Size Types for Implicit Complexity (Long Version) .
- Patrick Baillot and Alexis Ghyselen, ESOP 2021 Types for Complexity of Parallel Computation in Pi-Calculus. .
- Patrick Baillot, Alexis Ghyselen and Naoki Kobayashi, CONCUR 2021 Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. .

- Implementation of some simple reinforcement learning algorithms in EFF here .

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

Y`alexis`

X`gmail`

Y`com) @ .`

Resume: Here