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.

翻译：参数化允许在不同数据结构的实现之间转移证明。λΠ-演算模理论是带有依赖类型和用户自定义重写规则的λ演算扩展。它是一个逻辑框架，用于在不同证明系统之间交换证明。受参数化启发，我们定义了λΠ-演算模理论中理论的解释。这种解释允许在具备命题与证明概念的理论之间免费转移证明，前提是源理论能够嵌入到目标理论中。