Description

Les systèmes de preuve, automatisés ou interactifs, ont des applications croissantes dans l'éducation, l'industrie et la recherche. Bien que l'interopérabilité soit une propriété très importante en ingénierie et en informatique pour réduire les coûts de développement, elle est peu développée au sein des systèmes de preuve. Cela freine grandement la démocratisation de ces outils et la formalisation de résultats mathématiques avancés. Une façon d'améliorer l'interopérabilité est de développer des traductions entre systèmes. Mais pour que les définitions et les théorèmes traduits soient facilement utilisables, les types et fonctions traduits doivent être alignés avec ceux déjà utilisés dans les systèmes cibles. Pour cela, il est nécessaire de prouver qu'un type ou une fonction peut être substitué par un autre. Cependant, pour que cela soit correct, il faut montrer que les deux types sont bien isomorphes et que les deux fonctions sont bien égales. Ce projet vise à développer des outils permettant d'automatiser autant que possible ce type de preuves.

Compétences requises

Formation en logique. Expérience avec un assistant de preuve.

Bibliographie

Translating HOL-Light proofs to Coq, Frédéric Blanqui, LPAR, 2024.

Lambdapi export command, Lambdapi user manual, 2024

A modular construction of type theories, Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, LMCS 19(1), 2023.

Melham, T.F. (1989). Automating Recursive Type Definitions in Higher Order Logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds) Current Trends in Hardware Verification and Automated Theorem Proving. Springer, New York, NY.

Krauss, A. (2006). Partial Recursive Functions in Higher-Order Logic. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg.

Inductive types and recursive functions, Coq 8.20.0 reference manual, 2024.

Creating new tactics, Coq 8.20.0 reference manual, 2024.

Mots clés

preuve formelle, traduction de preuves, démonstration automatique, isomorphismes de type, égalité de fonctions, interopérabilité