Proofs for Free in the $λΠ$-Calculus Modulo Theory

TL;DR

This work develops a parametricity-inspired interpretation for theories within the $\lambda\Pi$-calculus modulo theory that feature a prelude encoding for propositions and proofs. By mapping source terms to larger target types with witnesses via $t^*$ and $t^+$, and by providing per-constant parameters, it enables proofs proven in a source theory to be carried over to a target theory when an embedding exists, along with a relative consistency guarantee. The paper formalizes the theory, the interpretation, and the required parameters, and showcases concrete embeddings such as natural numbers into integers and Zermelo set theory into pointed graphs, with a Dedukti implementation. This framework strengthens interoperability among proof systems by allowing automatic proof transfer across logically related theories while preserving typing and conversion through the translation. It also opens avenues for further theoretical work on normalization results for the $\lambda\Pi$-calculus modulo theory and its encodings.

Abstract

Parametricity allows the transfer of proofs between different implementations of the same data structure. The lambdaPi-calculus modulo theory is an extension of the lambda-calculus with dependent types and user-defined rewrite rules. It is a logical framework, used to exchange proofs between different proof systems. We define an interpretation of theories of the lambdaPi-calculus modulo theory, inspired by parametricity. Such an interpretation allows to transfer proofs for free between theories that feature the notions of proposition and proof, when the source theory can be embedded into the target theory.

Figures (1)

• Figure 1: Typing rules of the $\lambda\Pi$-calculus modulo theory.

Theorems & Definitions (19)

• Definition 1: Theory
• Lemma 1
• Definition 2: Theories with prelude encoding
• Example 1: Natural numbers
• Example 2: Integers
• Definition 3: Interpretation of terms
• Proposition 1
• proof
• Proposition 2
• proof