Dans cette thèse, nous étudions des méthodes se basant sur les types à taille et leur application notamment pour l’analyse de complexité en temps dans le pi-calcul. Le principe de ses types à taille est de suivre la taille des valeurs utilisées dans un programme afin de contrôler la récursion, et donc d’en déduire des bornes de complexité.
Dans un premier temps, nous montrons que l’on peut combiner ces types à taille avec la logique linéaire élémentaire afin de donner une caractérisation des classes de complexité 2k-EXP. Ensuite, nous utilisons ces types à taille pour un langage parallèle, le pi-calcul. Nous définissons d’abord deux notions de complexité pour ce langage : la complexité séquentielle (work) et la complexité parallèle (span). La première étant facilement définissable, nous proposons cependant pour la seconde une nouvelle définition équivalente à la complexité causale de la littérature mais plus facile d’utilisation pour notre étude, en se basant sur une sémantique opérationnelle simple. Nous proposons ensuite des systèmes de types tels que, à partir d’un typage d’un processus, on puisse extraire une borne de complexité en temps pour ce processus. Nous donnons tout d’abord, un premier système pour le work se basant sur les types à taille et les types input/output du picalcul, puis une modification de ce système permettant de traiter le span grâce à des informations de temps.
Enfin, nous proposons, dans une collaboration avec Naoki Kobayashi, un système de type pour le span plus expressif que le précédent, se basant sur le principe des usages : une méthode de typage utilisée pour étudier les deadlocks que nous adaptons à l’étude de la complexité.
Gratuit
Disciplines