École Nationale Supérieure de
Techniques Avancées

Résumé

Ce travail se concentre sur l'amélioration de l'interopérabilité des assistants de preuve par le biais de la traduction automatique. Il traite en particulier de l'alignement des définitions des réels entre HOL-Light et Coq. Ces assistants de preuve sont importants dans la vérification formelle des théorèmes mathématiques, mais leurs logiques fondamentales différentes créent des défis significatifs pour l'interopérabilité. Le projet vise à contribuer aux efforts en cours pour automatiser la traduction des preuves et des structures mathématiques entre ces systèmes, en particulier l'extension de l'outil de traduction hol2dk. Ce rapport résume le travail effectué dans le cadre d'un projet de stage. Il décrit comment la structure des nombres réels de HOL-Light a été dupliquée dans Coq afin d'être alignée avec la bibliothèque standard de Coq et de permettre ainsi une traduction aisée des preuves de nombres réels.