*Abstract:*

We define the typed lambda calculus *F*^{w}*/\* , a natural
generalization of Girard's system *F*^{w} with intersection types and bounded
polymorphism. A novel aspect of our presentation is the use of term
rewriting techniques to present intersection types, which clearly
splits the computational semantics (reduction rules) from the
syntax (inference rules) of the system. We establish properties
such as Church-Rosser for the reduction relation on types and
terms, and Strong Normalization for the reduction on types. We
prove that types are preserved by computation (Subject Reduction
property), and that the system satisfies the Minimal Types
property. On the way to establishing these results, we define
algorithms for type inference and subtype checking.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file