Proofs for Free in the $\lambda\Pi$-Calculus Modulo Theory

TL;DR

This paper introduces an interpretation method for the lambdaPi-calculus modulo theory that leverages parametricity to transfer proofs between different theories with dependent types and rewrite rules, enhancing proof interoperability.

Contribution

It presents a novel parametricity-inspired interpretation for the lambdaPi-calculus modulo theory, enabling proof transfer between embedded theories.

Findings

Proof transfer is possible between theories with embedded propositions and proofs.

The interpretation facilitates proof reuse across different proof systems.

The approach extends the logical framework's capabilities for proof exchange.

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.