TypiCal

L'interaction entre assistants de preuves peut permettre d'utiliser des théorèmes "aisément" prouvés dans un assistant de preuve donné, dans un autre assistant de preuve dans lequel ils auraient été plus difficiles à prouver. Cependant, les systèmes de preuves peuvent parfois être très différents.

Dans cet exposé, je présenterai une méthode pour importer des preuves de HOL-Light en Coq, basée sur la réflection. Après avoir présenté HOL-Light rapidement, j'expliquerai comment d'une part construire un modèle de HOL-Light en Coq prouvé correct, d'autre part enregistrer et exporter les termes de preuve de HOL-Light.