Decidable Higher Order Subtyping
Adriana CompagnoniAbstract:
This paper establishes the decidability of typechecking in Fw/\ (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.
ECS-LFCS-97-365.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