Decidability for Non-Standard Conversions in Typed Lambda-Calculi

This thesis studies the decidability of conversions in typed
lambda-calculi, along with the algorithms allowing for this
decidability. Our study takes in consideration conversions going
beyond the traditional beta, eta, or permutative conversions (also
called commutative conversions). To decide these conversions, two
classes of algorithms compete, the algorithms based on rewriting,
here the goal is to decompose and orient the conversion so as to
obtain a convergent system, these algorithms then boil down to
rewrite the terms until they reach an irreducible forms; and the
"reduction free" algorithms where the conversion is decided
recursively by a detour via a meta-language. Throughout this
thesis, we strive to explain the latter thanks to the former.