[TYPES] CORRIGENDA: completeness of subtype judgments

[Giuseppe Castagna]

Giuseppe Castagna wrote:
>> 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
> 


I am sorry Sophia, I have done a slight confusion, since I thought you 
were speaking of pi-calculus (because of the proximity of a mail in by 
mailbox asking references on it). What I said in my previous mail does 
apply to your question, but if you were thinking of lambda-calculus 
rather than pi-calculus, then there is much a better reference, that is 
"Semantic subtyping", another LICS paper (LICS 2002) by Alain Frisch, 
Veronique Benzaken and myself. It is available at

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

Here we consider a lambda calculus with the following (possibly 
recursive) types:

t ::=  t -> t  |  t x t  |  t\/t  |   t/\t  |  not(t) | Top


and which is complete with respect to the interpretation of types you asked

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

where v ranges over values.
So arrow types are interpreted as set of (closed) lambda-expressions of 
that type, and combinators are once more interpreted as the 
corresponding set-theoretic operations.

This paper is very technical too, in particular there is a circularity 
between the definition of [[t]] = { v | v:t } and the subtyping relation 
which cannot be dealt in a straightforward way. More generally, this 
relates to the difficulty of giving a set-theoretic interpretation of 
arrow types (this is *not* a term model).
Therefore if you want to have an idea about the general technique, I 
*strongly* suggest first to consult my joint keynote talk at ICALP 2006 
and PPDP 2006 "A gentle introduction to semantic subtyping" available at

   http://www.di.ens.fr/users/castagna/papers/icalp-ppdp05.pdf

Further insight is given by the ICTCS paper I cited in my previous mail, 
mail that is of course valid for what concerns your topic for concurrent 
languages. A journal version of the cited work in LICS 2002 should be 
ready in few days and I will be happy to send it to all persons interested

---Beppe---