Expressing Predicate Subtyping in Computational Logical Frameworks

Safe programming as well as most proof systems rely on typing.
The more expressive a type system is, the more extensively types can be
used to encode invariants that can be verified mechanically by 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 the 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 that can add syntactic markers
to make subtyping explicit in terms. This transformation is used to
translate the standard library of PVS, a proof assistant which uses
predicate subtyping extensively, into Dedukti.

Referente : Maria Paola Bonacina