Term transformation and proof (re)construction

Find more details here.

Level: L3-M2

Supervisor: Frédéric Blanqui and Gabriel Hondet

Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette, France.

Context: In the wake of the automation of the verification of formal proofs, many proof assistants have arised, such as Coq, Lean, Matita, the HOL family, Isabelle, PVS, etc. Formal proofs are used in mathematics but also in industry.

Proofs developed in these assistants are seldom interoperable due to the fact that the relationships between the theories these proof assistant implement in practice are rarely known. Combining the features of several proof assistants requires to translate their features in a common formalism and then ensure that these feature do not make the logic inconsistent.

The λΠ-calculus modulo rewriting (LPMR) is a logical framework allowing users to define their own logic and represent the proofs in those logics [1,2]. It is thus an adequate common language to express the features of proof assistants. For instance, one can represent in LPMR first-order logic and its proofs, simple type theory and its proofs, the Isabelle logic and its proofs [5], the Coq logic and its proofs [3], the Agda logic and its proofs [6], etc. In addition, there are a number of tools to transform those proofs and translate them back to various other systems: HOL-Light, Coq, PVS, Lean, etc. [7].

Dedukti is a type (or proof) checker for the LPMR. It shines when verifying that a theory expressed in LPMR is well-formed, but it is not suited for interactive development because of its lack of features. On the other hand, Lambdapi is a proof assistant for LPMR, able to read and generate Dedukti files. It features commodities such as tactics, implicit arguments, unification and deferred goals.

Objectives: In recent developments, some proof translators use tactics to reconstruct proofs. The goal of this internship is to develop proof reconstruction as well as simple proof generation tools like:

  • Extend the Lambdapi tactic why3 which calls SMT solvers through the Why3 API to solve arithmetic goals, where arithmetic symbols are defined in some user-supplied LPMR theory,
  • Develop a tactic for skolemisation and use SKonverto to generate a proof of a formula from a proof of its skolemized form.
  • Work on simple proof generation based on canonical solutions and type unification. For instance, given a proposition P, we may have in some database an axiom a:Prf P (the axiom a is a proof of P), then any goal of type Prf P can be automatically solved using the axiom a. This mechanism could be used to automatically infer inhabitants of some types.
  • Work on generic term translations from arbitrary logics to first order logic with prenex polymorphism understood by Why3: given any term t in some rich logic L, implement a transformation T from L to first order logic so that T(t) can be fed to SMT solvers [8]. The transformation from PVS-Cert to STT exposed in [9] is such a transformation, and would fit in the developments around PVS. The transformation would be used to translate PVS sequents into automatically provable formulas to be able to reconstruct proofs from the traces generated by PVS.

Workplan: The intern will start by getting accustomed to the notions of logical frameworks and dependent types. Then some simple coding tasks can be performed to get acquainted with the code related to tactics in Lambdapi (such as the first item of the list above). Finally the intern may choose among the other goals the one that suits them most.

Requirements: Basic knowledge of logic (e.g. Prolog) and typed λ-calculus.

Possible following: Extend Lambdapi with a general type-class mechanism, possibly using rewriting techniques.


[1] Dedukti: a logical framework based on the λΠ-calculus modulo theory, A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard, Draft, 2016.

[2] Some axioms for mathematics, F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet and F. Thiré, FSCD 2021.

[3] Higher-Order Confluence and Universe Embedding in the Logical Framework, Gaspard Férey, PhD, 2021.

[4] Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory, Gabriel Hondet and Frédéric Blanqui, TYPES'20.

[5] Translating proofs between Isabelle and Dedukti, Yann Leray, M1 Internship Report, 2021.

[6] Encoding Agda Programs Using Rewriting, G. Genestier, FSCD'20.

[7] Sharing a Library between Proof Assistants: Reaching out to the HOL Family, François Thiré, LFMTP'18.

[8] Interoperability between proof systems using the logical framework Dedukti, François Thiré, PhD thesis, 2020.

[9] Extending higher-order logic with predicate subtyping: Application to PVS, Frédéric Gilbert, PhD thesis, 2018.