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

uniqueprogram 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):

- Roberto Di Cosmo (Président du jury)
- Gilles Dowek
- Olivier Laurent
- Sam Lindley (Rapporteur)
- Dale Miller (Rapporteur)
- Didier Rémy (Directeur de thèse)