Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Verifiable certificates for predicate subtyping

Frédéric Gilbert 1
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a solution to this issue with a minimal formalization of predicate subtyping, named PVS-Core, together with a system of verifiable certificates for PVS-Core, named PVS-Cert. PVS-Cert is based on the introduction of proof terms and explicit coercions. Its design is similar to that of PTSs with dependent pairs, at the exception of the definition of conversion, which is based on a specific notion of reduction → β * , corresponding to β-reduction combined with the erasure of coercions. The use of this reduction instead of the more standard reduction → βσ allows to establish a simple correspondence between PVS-Core and PVS-Cert. On the other hand, a type-checking algorithm is designed for PVS-Cert, built on proofs of type preservation of → βσ and strong normalization of both → βσ and → β *. Using these results, PVS-Cert judgements are used as verifiable certificates for predicate subtyping. In addition, the reduction → βσ is used to define a cut elimination procedure adapted to predicate subtyping. Its use to study the properties of predicate subtyp-ing is illustrated with a proof of consistency.
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download
Contributor : Frédéric Gilbert <>
Submitted on : Thursday, January 10, 2019 - 7:35:12 PM
Last modification on : Tuesday, July 7, 2020 - 11:52:47 AM
Long-term archiving on: : Thursday, April 11, 2019 - 6:39:54 PM


Files produced by the author(s)


  • HAL Id : hal-01977585, version 1


Frédéric Gilbert. Verifiable certificates for predicate subtyping. 2019. ⟨hal-01977585⟩



Record views


Files downloads