Supervisor: Frédéric Blanqui
Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette
Keywords: logic, proof, interoperability, type theory
Description: This project is about formal proofs as digital objects, more specifically the translation of formal proofs between different proof systems. Formal proofs are used in mathematics but also in the industry for certifying the correctness of protocols, software and hardware. Interoperability is a very important feature in computer science and engineering to avoid useless work duplication and allow more safety. Unfortunately, interoperability between proof systems is not well developed. The λΠ-calculus modulo rewriting, and its implementation Dedukti, is a powerful logical framework allowing users to define their own logic and represent the proofs in those logics. Various proof libraries have already been represented in Dedukti. The objective of this PhD subject is to convert some of these libraries to a different proof assistant so that one gets something that is readable and readily usable by the users of the target system. This in particular requires to align the definitions of types and functions of the source and target systems like, for instance, the type of real numbers and the structures of groups, rings, etc.
Context: This project is about formal proofs as digital objects, more specifically the translation of formal proofs between different proof systems. Formal proofs are used in mathematics but also in the industry for certifying the correctness of protocols, software and hardware. Interoperability is a very important feature in computer science and engineering to avoid useless work duplication and allow more safety. Unfortunately, interoperability between proof systems is not well developed. The λΠ-calculus modulo rewriting, and its implementation Dedukti, is a powerful logical framework allowing users to define their own logic and represent the proofs in those logics. For instance, one can represent in Dedukti first-order logic and its proofs, simple type theory and its proofs, the Isabelle logic and its proofs, the Coq logic and its proofs, the Agda logic and its proofs, etc. In addition, there already exists a number of tools for transforming those proofs and translate them back to various other systems, e.g. STTfaXport and Lambdapi. There exist several tools for checking the correctness of Dedukti files: dkcheck, kontroli and lambdapi. While dkcheck and kontroli are mere checkers taking complete Dedukti files as input, Lambdapi is a proof assistant featuring implicit arguments, type inference, coercions, tactics, the possibility of calling external automated theorem provers, etc. for building Dedukti proofs interactively.
Objectives: Various proof libraries have already been represented in Dedukti (Matita arithmetic library, HOL-Light libraries, parts of GeoCoq, Isabelle/HOL standard library). The objective of this PhD subject is to convert some of these libraries to a different proof assistant, for instance, to translate the representation in Dedukti of some HOL-Light or Isabelle/HOL libraries in Coq or Lean, and to translate the representation in Dedukti of some Coq or Lean libraries to HOL-Light or Isabelle/HOL, so that one gets something that is readable and readily usable by the users of the target system. This in particular requires to align the definitions of types and functions of the source and target systems like, for instance, the type of real numbers and the structures of groups, rings, etc.
Methods: One important difficulty is that proof systems may have incompatible features: their combination may be inconsistent. Therefore, to translate a proof from one system to the other, we need to analyze the features of the source system used in the proof and check whether they are compatible with the features of the target system. To this end, we will use the Dedukti logical framework developed in the team. Concerning the alignment of definitions, the student will continue the work done for the alignment of HOL-Light definitions in Coq, and extend it to real and complex numbers, and adapt it to Isabelle/HOL. The student will also try to develop tactics to help to prove the correctness of those alignments automatically, especially in the case of inductive types and recursive function definitions. Isabelle/HOL and Coq use type classes. The student will study how type classes are internally represented in Isabelle/HOL proofs, propose a representation in Dedukti and a translation to Coq. Another possible research topic is the translation of Coq or Lean proofs which may use first-class dependent types to HOL-Light or Isabelle/HOL, which are proof systems not featuring first-class dependent types. Some recent research results show however that dependent types can be simulated to some extent by using the locale mechanism of Isabelle. Another complementary line of research is to transform dependent types into non-dependent types with extra conditions (e.g. an array of size n can be replaced by a list with the extra condition that its length is equal to n).
References: