Supervisor: Frédéric Blanqui
Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette
Context: 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. This project aims at improving the interoperability between systems based on dependent type theory like Coq, Lean, Agda, Matita and PVS, and systems based on simple type theory like Isabelle/HOL and HOL-Light, by using Dedukti as intermediate language.
There already exist translators from systems based on simple type theory to systems based on dependent type theory. However, there is currently no translator in the other way around: from systems based on dependent type theory to systems based on simple type theory. The problem is that systems based on simple type theory do not feature first-class dependent types. A dependent type is a type that can depend on some values. For instance, the type of vectors of some given dimension.
To translate the definitions and proofs of a system based on dependent type theory to a system based solely on simple type theory, one therefore has to find a way to eliminate the uses of dependent types. This might not be always possible, but we can look for a large enough class of definitions and proofs from which dependent types can be eliminated. For instance, the type of vectors of dimension n could be replaced by the subtype of lists of length n.
Objective: The long-term goal of this project is to translate to Isabelle or HOL-Light large libraries of definitions and proofs from Coq, Lean, Agda or Matita.
Work plan: The student will start by studying and translating by hand a number of simple statements and proofs that use dependent types. She could then try to design a general translation of some dependent type theory to simple type theory or some extension of it to represent Isabelle locales and type classes, and prove some of its properties. Finally, the student would then develop an implementation of this translation to Isabelle or HOL-Light, and apply it to actual libraries coming from Matita, Agda or Lean.
References: