*Abstract:*

This paper establishes the decidability of typechecking in
*F*^{w}*/\* (F-omega-meet), a typed lambda calculus
combining higher-order polymorphism, subtyping, and intersection
types. It contains the first proof of decidability of subtyping for
a higher-order system.

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