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 Rocq, Lean, Agda and Matita, by using Dedukti as intermediate language to factorize that work as much as possible.
Dedukti is a logical framework, that is, a language in which one can define the deduction rules and represent the proofs of different logical systems. It is based on the λΠ-calculus modulo rewriting. The λΠ-calculus is the simplest type system featuring both simple and dependent types. The λΠ-calculus modulo rewriting extends the λΠ-calculus by identifying types equivalent modulo user-defined rewriting rules, i.e. oriented equations. It is like working not with types but with equivalence classes of types modulo an equivalence relation.
The λΠ-calculus itself, without rewriting, is not very powerful: for instance, it is not possible to quantify over types and have type-polymorphic functions. However, with rewriting (at the type level), it is possible to represent the terms of polymorphic systems like Girard's system F and Coquand-Huet's Calculus of Constructions. Actually, it is possible to encode in Dedukti any functional pure type system [1].
The core of the type systems of Agda, Lean or Rocq is a functional pure type system with an infinite number of type constants Type0, Type1, ... called type universes that are linearly nested in one another (Type0 is in Type1, Type1 is in Type2, etc.) and so that every Typei is closed by dependent product, that is, if A is in Typei and B is an A-indexed family of types in Typej, then Πx:A,B (the functions from A to B) is in Typemax(i,j) (to avoid contradictions like with the set of all sets in set theory). (Roughly speaking, type universes correspond to nested inaccessible cardinals in set theory.) Because that core system is a functional pure type system, it can be encoded in the λΠ-calculus modulo rewriting. It can even be encoded using only a finite number of symbols and rules by representing natural numbers inductively.
But Agda, Lean and Rocq extends this core type system in many ways. For instance, Rocq adds a subtyping relation on universes called cumulativity which makes it non-functional: the elements of Typei are also in Typej for all j≥i. Lean and Rocq assumes that the first universe of the hierarchy, which is used to represent propositions, is impredicative, that is, Πx:A,B is in Type0 if B is in Type0. And Agda, Lean and Rocq allows users to quantify over universes in different ways.
All these extensions require to adapt the equivalence on types to take into account the algebraic properties of the max operator, cumulativity and impredicativity. This makes the encoding of universes in Dedukti more complicated since, in Dedukti, the equivalence relation on types must be decided by a terminating and confluent rewrite systems. This for instance requires the use of matching modulo associativity and commutativity [6], or of a particular rewriting strategy [7], to handle the max operator which is commutative and associative.
Several PhD works and publications have already been partially dedicated to this problem, and two tools have been developed to actually translate terms with universes to Dedukti: CoqInE for Rocq, and Lean2dk for Lean. The last version of CoqInE is based on the PhD work of Gaspard Férey in 2021 [5]. However, the type theory of Rocq and its implementation has evolved a lot since then so that the encoding of Rocq universes in Dedukti needs to be updated to take these changes into account.
While the case of predicative systems is more or less well understood now, the case of impredicative systems is not completely settled yet. A former PhD student, Yoan Géran, started to develop an encoding for a non-polymorphic impredicative universe system. Another current PhD student, Rishikesh Vaishnav, extended it to prenex polymophism and implemented it in lean2dk.
Objective: The goal of this project is to study whether the encodings that have been developed so far indeed allows one to efficiently encode and translate to other systems the existing libraries of Rocq proofs and, if not, propose some new encoding allowing to do so.
Work plan: 1) Study the different encodings and their properties. 2) Check the completeness of Géran's encoding and Vaishnav's extension. 3) Study whether that encoding can be simplified and extended to the Rocq universe system. 4) Update CoqInE and translate the whole Rocq standard library to Dedukti.
References: