[TYPES] Looking for a type system

[gc@pps.jussieu.fr]

David-Sarah Hopwood wrote:
> 
> Also
> 
> Giuseppe Castagna, Alain Frisch
> A Gentle Introduction to Semantic Subtyping
> <http://www.di.ens.fr/users/castagna/papers/icalp-ppdp05.pdf>
> 

Indeed. The reference above is, as the title goes, a gentle introduction that
avoids technicalities as much as possible. It is the right reference to have an
idea of the general framework. For the full story and gory details please refer to:

A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping: dealing
set-theoretically with function, union, intersection, and negation types.
Journal of the ACM, vol. 55, n. 4, pag. 1―64, 2008.
http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf

which contains the previous reference.

For polymorphism ... we are working on it: few key theorems still missing :-(

In the meanwhile if missing T->T is not a concern you can check this work by 
Hosoya (mainly)

H. Hosoya, A. Frisch, and G. Castagna: Parametric Polymorphism for XML. In 
POPL '05, 32nd ACM Symposium on Principles of Programming Languages, pag. 50-62, 
ACM Press, 2005.
http://www.pps.jussieu.fr/~gc/papers/popl05.pdf


---Beppe---

P.S. For the very few persons who may be interested, please notice that
http://www.di.ens.fr/users/castagna no longer is my home page. I moved two years
ago: http://www.pps.jussieu.fr/~gc