Date(s) - 04/12/2014
9 h 30 min - 11 h 00 min
Soutenance de thèse
We study in this thesis a semiring structure with a product based on the resolution rule of logic programming.
This mathematical object was introduced initially in the setting of the geometry of interaction program in order to model the cut-elimination procedure of linear logic.
It provides us with an algebraic and abstract setting, while being presented in a syntactic and concrete way, in which a theoretical study of computation can be carried on.
We will review first the interactive interpretation of proof theory within this semiring via the categorical axiomatization of the geometry of interaction approach. This interpretation establishes a way to translate functional programs into a very simple form of logic programs.
Secondly, complexity theory problematics will be considered: while the nilpotency problem in the semiring we study is undecidable in general, it will appear that certain restrictions allow for characterizations of (deterministic and non-deterministic) logarithmic space and (deterministic) polynomial time computation.
*Membres du jury :
– Pierre-Louis Curien
– Jean-Yves Girard (directeur de thèse)
– Ugo dal Lago (rapporteur)
– Paul-André Melliès
– Myriam Quatrini
– Ulrich Schöpp
– Philip Scott (rapporteur)
– Kazushige Terui
Lien : theses.fr