Encodage des systèmes de types avec univers dans Dedukti · Laboratoire Méthodes Formelles, Doctorat · La Géode