[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---
More information about the Types-list
mailing list