Skip to Main content Skip to Navigation
New interface
Conference papers

Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory

Gabriel Hondet 1 Frédéric Blanqui 1 
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
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.
Complete list of metadata

https://hal.inria.fr/hal-03279766
Contributor : Gabriel Hondet Connect in order to contact the contributor
Submitted on : Monday, October 25, 2021 - 10:30:39 AM
Last modification on : Friday, August 5, 2022 - 2:58:08 PM

Files

main.pdf
Files produced by the author(s)

Identifiers

Citation

Gabriel Hondet, Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. TYPES 2020 - 26th International Conference on Types for Proofs and Programs, Mar 2020, Turino, Italy. ⟨10.4230/LIPIcs.TYPES.2020.6⟩. ⟨hal-03279766v2⟩

Share

Metrics

Record views

86

Files downloads

90