2026-07-24T18:02:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13885 2024-03-06T10:52:43Z ddc:004 open_access

Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory Hondet, Gabriel Blanqui, Frédéric Predicate Subtyping Logical Framework PVS Dedukti Proof Irrelevance 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gabriel Hondet and Frédéric Blanqui 2021 Is Part Of LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2020.6 urn:nbn:de:0030-drops-138853 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.6 eng https://creativecommons.org/licenses/by/4.0/legalcode