[TYPES/announce] Paper announcement: Intersection and union types for lambdabar-mu-mutilde

[Steffen van Bakel]

Dear all,

I happy to announce my paper on intersection and union type assignment  
for Curien & Herbelin's calculus lambdabar-mu-mutilde (LMMT for  
short), that can be found at:

	http://www.doc.ic.ac.uk/~svb/Research/Papers/lmmtfull.pdf

In this paper, I study in detail the difficulties that arise when  
adding both intersection and union types to the highly symmetric  
sequent calculus LMMT.  I show that it is relatively easy to achieve  
subject expansion (completeness, preservation of types against  
reduction), but impossible to achieve subject reduction (soundness) in  
a meaningful way, i.e. in a way that preserves types assignable to  
lambda terms in the system of BCD.

I also show that only BCD types, equipped with a contra-variant  
partial order relation <=, are suited for LMMT.  For example, systems  
based on, for example, strict types or Krivine's system D (both not  
equipped with a contra-variant <=) would not suffice.  In the paper I  
give examples that show that a system based on the latter does not  
satisfy subject reduction; these can partially be overcome when using  
<=.  However, even when such a relation is present, the system is not  
sound.

The heart to the problem is that a mu-reduction towards an introduced  
intersection (the result of applying rule (\intR)) is not sound, and  
neither is a mutilde-reduction towards an introduced union.  Another  
way of stating this is: both rules

  Gamma | mutilde x.c : A |- Delta    Gamma |- mu alpha.c : A |- Delta
  --------------------------------    --------------------------------
      c : Gamma, x:A |- Delta           c : Gamma |-  alpha:A | Delta

are not admissible.

Two restrictions are presented, one restricting (\cap R) to values,  
and one restricting (\cup L) to linear contexts (slots), and I show  
that using these restrictions, subject reduction can be achieved for,  
respectively, CBV and CBN reduction, albeit at the loss of subject  
expansion.

Any comment or feedback is welcome.

Kind regards,
Steffen van Bakel

Department of Computer Science
Imperial College London
180 Queen's Gate
London SW7 2BZ UK

+ (44)(0) 20 7594 8263
www.doc.ic.ac.uk/~svb
svb at doc.ic.ac.uk