Internship subject: Term transformation and proof (re)construction


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:

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.

References:

[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.


Statcounter W3C Validator Last updated on 27 June 2022. Come back to main page.