[TYPES] completeness of subtype judgments

[Gerwin Klein]

Dear Sophia,

if I remember correctly, Alessandro Coglio had something like this for his JVM 
subroutine type system in 

A. Coglio, "Simple Verification Technique for Complex Java Bytecode 
Subroutines", Concurrency and Computation: Practice and Experience, 16
(7):647-670, 2004

Cheers,
Gerwin

On Wednesday 26 April 2006 06:21, Sophia Drossopoulou wrote:
>       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.