La théorie des types dépendants sert de fondations à une famille d'assistants à la preuve dont Agda, Coq et Lean sont trois représentants modernes. La correction de ces implémentations reposent sur des propriétés métathéoriques des systèmes de types dépendants telle que l'existence de formes canonique, la décidabilité de la conversion ou du typage, dont les preuves sont notoirement complexes. Dans cette présentation, j'expliquerai les difficultés qui se présentent pour méchaniser de telles preuves de propriété métathéorique ainsi que les solutions retenues pour établir formellement des résultats de normalisation et de décidabilité de la théorie des types de Martin-Löf dans l'assistant de preuves Coq. J'esquisserai comment ce projet donne aussi l'opportunité de développer des extensions expressives des assistants à la preuve tout en préservant des fondations solides.