Encoding of Predicate Subtyping with Proof Irrelevance in the $\lambda$$\Pi$-Calculus Modulo Theory
Logic in Computer Science
2021-10-27 v1
Abstract
The -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 -calculus modulo theory using rewriting.
Keywords
Cite
@article{arxiv.2110.13704,
title = {Encoding of Predicate Subtyping with Proof Irrelevance in the $\lambda$$\Pi$-Calculus Modulo Theory},
author = {Gabriel Hondet and Frédéric Blanqui},
journal= {arXiv preprint arXiv:2110.13704},
year = {2021}
}
Comments
TYPES 2020 wasn't held in Turin as planned because of the COVID-19 outbreak. TYPES 2020 - 26th International Conference on Types for Proofs and Programs, Mar 2020, Turino, Italy