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 two important proof
systems, Isabelle
and Coq.
isabelle_dedukti
is a tool that extracts proofs from Isabelle and translate them
to Lambdapi, a
language which, in turn, can be translated to Coq. There are however
several problems to solve to get something consistent, readily
usable, and that scales up:
Both Isabelle and Coq use an important mechanism to
structure formalizations: type classes and, more generally in
Isabelle, locales. Type classes are a restricted form of
locales enjoying some additional features. They are heavily
used to represent mathematical structures like groups, rings,
etc. However, the way proofs using locales are currently
translated is not fully compatible with the logic of Coq.
To get readily usable statements in Coq, it is necessary to
align the definitions of Isabelle with those already defined
in Coq. For instance, an Isabelle theorem on Isabelle natural
numbers should be translated to a Coq theorem on Coq natural
numbers, and not to a Coq theorem on the representation of
Isabelle natural numbers in Coq. To this end, Lambdapi can
replace an Isabelle symbol by a Coq expression. For instance,
the Isabelle symbol for the type of natural numbers by the Coq
symbol for the type of natural numbers, and the Isabelle
symbol for the addition on natural numbers by the Coq symbol
for the addition on natural numbers. But, for such a
replacement to be valid, one must prove that the Coq
expression satisfies the properties defining the Isabelle
symbol. For instance, that the type representing Isabelle
natural numbers in Coq is isomorphic to the Coq type of
natural numbers, and that the Coq addition on natural numbers
satisfies the property defining the Isabelle addition on
natural numbers.
In order for Coq to be able to check the translation of
large Isabelle libraries, it will probably be necessary to use
sharing techniques, split the big proofs in smaller parts, and
parallelize their translation and checking.
Objective: The long-term goal of this project is
to solve the above problems in order to get an automatic translation
to Coq of the whole Isabelle Archive of Formal Proofs.
Work plan: The student will start by studying
how proofs and type classes are represented by Isabelle and
currently translated to Lambdapi. She will then develop
transformations on the proofs in order to make them valid in
Coq. This will require to represent Isabelle type classes in Coq,
using Coq type classes or canonical structures, and
possibly hierarchy-builder. To
solve the second problem, the student will adapt to Isabelle the
mappings already developed
in hol2dk between
the proof
assistant HOL-Light,
which is very similar to Isabelle but does not feature type
classes. Finally, for the last problem, the student can take some
inspiration
from hol2dk.
