monotonic subtype relations?

Date: Wed, 10 Apr 91 10:38:53 EST

One of my students (David Wright) is looking at type inference including
needed reduction information (see Tapsoft 1991).  An interesting feature of 
the work is that there is a 'subtype' relation that is naturally covariant 
in the sense that a leq a' & b leq b' implies a->b leq a'->b'.  (The usual 
implication is that a'->b leq a->b'.)  
It would seem to follow that the 'simple semantics' is inappropriate
for this type system.  I (we) would appreciate any pointers to any relevant
papers that readers may be aware of that may help us develop the 'right'
semantics, or indeed, any references to work involving such monotonic type
relations.  Suggestions most welcome.

Clem Baker-Finch			AARNet: clem@ise.canberra.edu.au
Information Sciences & Engineering	Phone:  +61 6 2522408
University of Canberra			Fax:    +61 6 2522191
PO Box 1, Belconnen
A.C.T.  Australia   2616