My PhD thesis was supervised by Didier Rémy, defended on March 30th, 2016, and is titled
Which types have a unique inhabitant?
Focusing on pure program equivalence
An online manuscript can be found there:
thesis-manuscript.pdf
I occasionally update the manuscript to fix mistakes and clarify
formulas; any feedback is warmly welcome.
The slides of my defense talk (in english) are also available there:
soutenance.pdf
Abstract:
Some programming language features (coercions, type-classes, implicits) rely on inferring a part of the code that is determined by its usage context. In order to better understand the theoretical underpinnings of this mechanism, we ask: when is it the case that there is a unique program that could have been guessed, or in other words that all possible guesses result in equivalent program fragments? Which types have a unique inhabitant?
To approach the question of unicity, we build on work in proof theory on more canonical representation of proofs. Using the proofs-as-programs correspondence, we can adapt the logical technique of focusing to obtain more canonical program representations.
In the setting of simply-typed lambda-calculus with sums and the empty type, equipped with the strong beta-eta-equivalence, we show that uniqueness is decidable. We present a saturating focused logic that introduces irreducible cuts on positive types “as soon as possible”. Goal-directed proof search in this logic gives an effective algorithm that returns either zero, one or two distinct inhabitants for any given type.
I was honored by the presence of the following thesis commitee (Jury):