Interoperability of proofs with Dedukti and Beluga

Critical systems such as transportation systems require a high level of safety that can only be achieved with formal proof. Such formal proofs are typically expressed in some logic that can be verified by theorem provers. The diversity of theorem provers and logics has a negative consequence: the same theorem is proved many times and it is difficult for these systems to co-operate, because they do not implement the same logic. Logical frameworks are a class of theorem provers that overcome this issue by providing a generic framework in which we can represent and specify various logics. The logical framework Dedukti developed at INRIA shines when it comes to compactly represent logics using user-defined rewrite rules, but lacks the ability to write proof transformations between logics. The logical framework Beluga developed at McGill excels in writing such proof transformations, but does not allow user-defined rewrite rules. This project aims at building a new logical framework combining the strengths of Dedukti and Beluga. Concretely, we plan to first design a unified logical framework that supports both user-defined rewrite rules and the ability to write proof transformations.

Faculty Supervisor:

Brigitte Pientka

Student:

François Thiré

Partner:

Discipline:

Computer science

Sector:

University:

Program:

Globalink Research Award