[TYPES] Formal treatment of intersection/union/arrow subtyping?

[Mariangiola Dezani]

About losing subject reduction in presence of intersection/union/arrow  
I suggest
also to look at:

M. Dezani-Ciancaglini and S. Ronchi Della Rocca.  Intersection and  
Reference Types,
http://www.di.unito.it/~dezani/papers/dr.pdf

which discusses (1)  S->T1 & S->T2 <: S->(T1 & T2)

S. van Bakel. Subject Reduction vs Intersection / Union Types for  
lambda-bar-mu-mu-tilde
http://www.doc.ic.ac.uk/~svb/

which shows that subject reduction does not hold without assuming  
subtyping involving arrows.

Best,

Mariangiola

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

Mariangiola Dezani-Ciancaglini
Dipartimento di Informatica
Universita' di Torino
c.Svizzera 185, 10149 Torino (Italy)

e-mail :  dezani at di.unito.it
phone: 39-011-6706732
fax : 39-011-751603
mobile: 39-320-4359903 (preferred) 39-348-2251592

http://www.di.unito.it/~dezani

**********************************************************************
Unless unavoidable, no Word, Excel or PowerPoint attachments, please.
See http://www.gnu.org/philosophy/no-word-attachments.html
**********************************************************************

"L'ITALIA RIPUDIA LA GUERRA come strumento di offesa alla libertà  
degli altri
popoli e come mezzo di risoluzione delle controversie internazionali."
(Art. 11 della Costituzione della Repubblica Italiana)