En mathématiques comme en informatique, il est d’usage de faire appel à des outils numériques de vérification pour augmenter la confiance dans les preuves et les logiciels. La pratique la plus commune est le test, mais elle est limitée. Les assistants de preuve interactifs sont des outils permettant d’effectuer des preuves avec une grande confiance, laissant l’humain trouver les idées des preuves tout en vérifiant méticuleusement que toutes les étapes de la preuve sont valides. Cette thèse s’inscrit dans une lignée de travaux visant à automatiser les preuves, avec l’objectif final de répandre l’usage des assistants de preuve à la place du test logiciel, partout où cela est possible et pertinent. On s’intéresse ici au partage de théorie formelle entre plu- sieurs représentations différentes d’un même concept mathématique, ou plusieurs implémentations d’une même spécification. Sur le plan théorique, cette étude s’appuie sur l’ana- lyse de traductions de paramétricité pour le Calcul des Constructions, et en propose une généralisation. Ces résultats s’incarnent dans la conception de deux outils de transfert de preuve, TRAKT et TROCQ, dont on discute ici l’implémentation, à l’aide du méta-langage COQ-ELPI.