Expressing Predicate Subtyping in Computational Logical Frameworks
by Gabriel Hondet
Tuesday 27 September 2022 at 5pm
ENS Paris-Saclay, Room 1Z14
Abstract: Safe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Predicate subtyping extends simple type theory by allowing terms to be defined by predicates. A predicate subtype { x : A | P(x) } is inhabited by terms t of type A for which P(t) holds. This extension provides a rich and intuitive but undecidable type system.
This work is dedicated to the encoding of predicate subtyping in Dedukti: a logical framework with computation rules. We begin by encoding explicit predicate subtyping for which terms of type A are syntactically different from terms of type { x : A | P(x) }.
Predicate subtyping, is often used implicitly, with no syntactic difference between terms of type A and terms of type { x: A | P(x) }. We enrich our logical framework with a term refiner which can add these syntactic markers in order to explicit subtyping in terms. This transformation is used to translate the standard library of PVS, a proof assistant extensively using predicate subtyping, to Dedukti.