Skip to Main content Skip to Navigation

Sized Types Methods and their Applications to Complexity Analysis in Pi-Calculus

Alexis Ghyselen 1, 2
2 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : 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. Several methods have been proposed to characterize time complexity classes. One approach comes from linear logic and restricted versions of its !-modality controlling duplication. Another approach 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. We design a type system for an abstract functional language allowing non-linear functional arguments, with a seemingly good intensional expressivity. Our approach relies on elementary linear logic, combined with a system of linear sized types. We discuss the expressivity of this new type system 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.
Complete list of metadata
Contributor : Abes Star :  Contact
Submitted on : Wednesday, October 27, 2021 - 3:10:21 PM
Last modification on : Friday, October 29, 2021 - 3:49:12 AM


Version validated by the jury (STAR)


  • HAL Id : tel-03405961, version 1


Alexis Ghyselen. Sized Types Methods and their Applications to Complexity Analysis in Pi-Calculus. Computational Complexity [cs.CC]. Université de Lyon, 2021. English. ⟨NNT : 2021LYSEN036⟩. ⟨tel-03405961⟩



Record views


Files downloads