# [TYPES] CORRIGENDA: completeness of subtype judgments

Giuseppe Castagna Giuseppe.Castagna at ens.fr
Wed Apr 26 07:43:08 EDT 2006

```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---
```