The $\lambda$$\Pi$-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper, we show how to encode predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. We prove that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the $\lambda$$\Pi$-calculus modulo theory using rewriting.

翻译：$\ lambda$\ Pi$- calculus modulo 理论是一个逻辑框架,在这个框架中,各种逻辑和类型系统可以编码,从而帮助基于这些逻辑和类型系统的验证系统的交叉验证和互操作性。在本文中,我们展示了如何编码上游亚缩和证据无关性,这是PVS 验证助理的两个重要特征。我们证明这一编码是正确的,编码证据可以由Dedukti进行机械检查,Dedukti是使用重写对 $\ lambda$\ Pi$\ Pi$- calcululs 模型理论进行字型检查的。