[TYPES] completeness of subtype judgments

[Sophia Drossopoulou]

Dave Clarke and I have been wondering whether there is any work
on the completeness of type systems, in the presence of subtyping
and rather intricate types.

We have a way of defining what completeness is, but proving it for
a  particular system seems daunting.

Here is how we would define completeness of a type system:

      1) Define a judgment \Gamma |- T <: T’ with the obvious meaning

      2) Define the denotation of a type T for a given stack S
         and heap H, as
                             [[T]]_{S,H}
         as the set of all values with type T in S and H.
        (We need to consider the stack S because we have path-dependent
         types, i.e.  T may mention entities from S.)

      3) Define a judgment \Gamma |- S, H to express when a
         stack S and heap H agree with an environment \Gamma.

      4)  The subtyping system is complete, iff
          \forall \Gamma, T and T’
              (\forall S, H:
               \Gamma |- S,H => [[T]]_{S,H} \subset [[T’]]_{S,H} )
              =>
              ( \Gamma |- T <: T’ )

Our question is whether there are alternative formulations of
completeness, and, more importantly, whether there is work proving
such completeness.

Cheers and thanks,

Dave Clarke and Sophia Drossopoulou

-- ===================================================================
Sophia Drossopoulou Department of Computing,
http://www.doc.ic.ac.uk/~scd/index.html