[TYPES] completeness of subtype judgments

[Giuseppe Castagna]

Sophia Drossopoulou wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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.
> 

Yes definitively there is one!

In our paper at LICS 2005, Rocco De Nicola, Daniele Varacca, and I 
defined a subtyping relation for the following types for the pi-calculus

    t ::= ch+(t)  | ch-(t)  |  t\/t  |   t/\t  |  not(t) | Top

which is complete with respect to the following interpretation of types

[[t]] = { v | v:t }

more precisely, [[ ch+(t) ]] is the set of all channels [1] on which you 
can receive message of type t, [[ ch+(t) ]] is the set of all channels 
[1] on which you can safely write message of type t, while the 
combinator have set theoretic interpretation, that is [[s \/ t ]] is the 
union of [[s]] and [[ t ]], [[s /\ t ]] is the intersection of [[s]] and 
[[ t ]], and [[not(t)]] is the complement of [[t]] with respect to the 
set of all (well-typed) values.

I guess this is exactly what you were asking for.

The paper is available on line at

http://www.cduce.org/papers/semantic_pi.pdf

it is a little bit technical. If you want to have a much less technical 
introduction you can consult my invited paper at ICTCS "Semantic 
subtyping: challenges, perspectives, and open problems" (LNCS available 
on line at

ftp://ftp.di.ens.fr/pub/users/castagna/ictcs05a.pdf

Also, Mariangiola Dezani, Daniele Varacca and I studied the "local" 
variant (you cannot read on an input channel, that is you do not have 
the ch+(t) type) of the above calculus and proved how it can 
type-faithfully encode a lambda-calculus with union intersection 
negation arrow products and recursive types. The local variant is quite 
interesting because the subtyping relation is *far* simpler and more 
tractable that the full case (though the latter is decidable). The paper 
is currently under submission but it is accessible (though not 
publicized) at the following URL:

ftp://ftp.di.ens.fr/pub/users/castagna/cpi-encode.pdf

Comments and suggestions are very welcome.

---Beppe---


[1] Channels here are intended as channel /names/, which must thus be 
differentiated from channel /variables/, since values must be closed. In 
practice for channel names we use the standard definition given by 
Barendregt for for lambda-calculus names, that is channels which cannot 
be substituted.