Makni, Mme Amal (2024) The translation of real numbers from HOL-Light to Coq. PRE - Research Project, ENSTA.

[img]
Preview
Archive (ZIP)
534Kb

Abstract

This work focuses on improving the interoperability of proof assistants through automated translation. Particularly, it addresses the alignment of real number definitions between HOL-Light and Coq. These proof assistants are important in the formal verification of mathematical theorems, but their different foundational logics create significant challenges to interoperability. The project aims to contribute to ongoing efforts to automate the translation of proofs and mathematical structures between these systems, particularly the extension of the translation tool hol2dk. This report summarizes the work conducted during an internship project. It describes how HOL-Light's structure of real numbers was duplicated in Coq so as to be aligned with Coq's standard library and hence allowing the smooth translations of real number proofs.

Item Type:Thesis (PRE - Research Project)
Uncontrolled Keywords:Proof Assistants, Interoperability, HOL-Light, Coq, Real Numbers, hol2dk, Proof Translations.
Subjects:Information and Communication Sciences and Technologies
ID Code:10028
Deposited By:Omar Makni
Deposited On:02 sept. 2024 12:51
Dernière modification:02 sept. 2024 12:51

Repository Staff Only: item control page