Encoding of Predicate Subtyping with Proof Irrelevance in the $\lambda$$\Pi$-Calculus Modulo Theory

TL;DR

This paper presents a method to encode predicate subtyping and proof irrelevance within the λΠ-calculus modulo theory, enabling cross-verification of proof systems and proof checking via Dedukti.

Contribution

It introduces a novel encoding of predicate subtyping and proof irrelevance in the λΠ-calculus modulo theory, with proven correctness and mechanical proof checking capabilities.

Findings

Encoding is correct and sound.

Proofs can be mechanically checked in Dedukti.

Enhances interoperability of proof systems.

Abstract

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.