Thursday 23 March 2017, 14:00: Extending Higher-order Logic with Predicate Subtyping, Frédéric Gilbert (Deducteam).

Predicate subtyping is an extension of higher-order logic where the grammar of types is enriched with a construction for restricted comprehension allowing to define, for any type A and any predicate P on A, a new type {x : A | P}. The inhabitants of such a type are the inhabitants t of A for which P(t) is provable. As a consequence, type-checking becomes undecidable.

We present a possible formalization of predicate subtyping, which can be the base of a formalization of the proof assistant PVS. We also present a similar system using explicit proofs and coercions. This system is used as a lightweight language for predicate subtyping. It is also a first step towards the expression of predicate subtyping in a universal system.