Abstract

The talk is closely related to the talk I am going to present with Zhaohui Luo at "Types" meeting. Here I'll pay more attention to the proof-theoretical (and technical) side.

A basic idea behind coercive subtyping is that subtyping provides a powerful mechanism for notational abbreviation in type theory. This abbreviational mechanism is formally treated at the level of the logical framework LF -- the meta-level language used to specify type theories. Given two kinds (meta-level types) K and K', where K is a (proper) subkind of K' and a functional operation f whose source kind is K', one can apply f to any object a of kind K as well as those of kind  K'. The meaning of such an application is that f(a) is definitionally equal to f(c(a)), where c is the coercion between K and K'.

In addition to (standard) declarations of constants and computational rules we consider subtyping declarations of the form A<_c B:Type, where A, B are types, and c is a coercion term (representing "embedding" of A into B). LF is extended by the rules that provide "lifting" of subtyping to the level of kinds, the rules for product-introduction and transitivity. The rules for coercive application make possible formation of the expressions like f(k) instead of f(c(k)) and the coercive definition rule equates f(k) and f(c(k)).

The results presented in the talk will be in a sense "orthogonal" to the ones that are based on normalisation techniques, and show what may be done without any assumptions about normalisation properties of a type theory T specified in LF. In particular, main attention is paid to the conservativity properties of the theory including coercions with respect to the theory where coercion declarations are omitted, and their connection with coherence of coercion declarations.