[TYPES] completeness of subtype judgments
Giuseppe Castagna
Giuseppe.Castagna at ens.fr
Wed Apr 26 05:56:59 EDT 2006
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.
More information about the Types-list
mailing list