Systèmes de preuve interopérables.

Developments of formal specifications and proofs have spectacularly blossomed over the last decades, hosted by a diversity of frameworks, systems and communities. And yet, the heterogeneity of these environments has hindered some fundamental steps in the scientific process: the sharing and reuse of results. This dissertation proposes a way of distributing the same formal development between various proof systems, thus augmenting their interoperability. Chapters 1 and 2 present the logical framework that is used to centralize the formal specifications and proofs. In particular, it is based on a variation of the λµ˜ µ-calculus designed to support interactive proof developments. Chapters 3 and 4 develop the rewriting and categorical structures required to give strict semantics to proof languages. Based upon these first results, chapters 5 and 6 respectively use a type system for proof languages to secure a type safety proposition, and expose a series of translations of the centralized developments into other major formal frameworks. Among other things, the latter contributes to a simplification of Frege Hilbert deduction systems. Finally, chapters 7 and 8 deal with the problems arising from the implementation of our centralized proof development system. Of special notice is the presentation of a theory of classes, that allows for the finite first-order expression of axiom schemes.Les developpements de specifications et des preuves formelles ont pris de l'ampleur durant les dernieres decennies, elabores au sein d'une diversite de canevas, de systemes et de communautes. Cependant l'heterogeneite de ces environnements gene quelques-unes des etapes fondamentales du processus de reflexion scientifique : le partage et la reutilisation des resultats. Cette dissertation propose une methode de distribution du meme developpement formel entre de divers systemes de preuve, augmentant ainsi eur interoperabilite. es chapitres 1 et 2 presentent le cadre logique qui est employe pour centraliser les specifications et les preuves formelles. Sa principale contribution est une ariation du λµ˜ µ-calcul conçu pour supporter le eveloppement interactif de preuves. Les chapitres 3 et 4 developpent les structures de recriture et categoriques necessaire a l'expression formelle de la semantique des langages de preuve. Base sur ces premiers resultats, le chapitre 5 utilise un systeme de types pour des langages de preuve pour asseoir un propriete de surete de typage, et le chapitre 6 expose une serie de traductions des developpements centralises dans d'autres cadres formels majeurs. Entre autres, le dernier contribue a une simplification des systemes de deduction a la Frege-Hilbert. En conclusion, les chapitres 7 et 8 s'interessent aux problemes resultant de l'implementation de notre systeme de developpement centralise de preuve. Ainsi, celui-ci decrit les details du logiciel cree, et celui-la fait la presentation d'une theorie de classes qui permet l'expression finie au premier ordre de schemas d'axiomes