%0 Conference Proceedings
%F dhm95b
%A Dussart, Dirk
%A Henglein, Fritz
%A Mossin, Christian
%T Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time
%B Proc.\ 2nd Int'l Static Analysis Symposium (SAS), Glasgow, Scotland
%P 118-135
%S Lecture Notes in Computer Science
%I Springer-Verlag
%X The combination of parameter polymorphism, subtyping ex- tended to qualified and polymorphic types, and polymorphic recursion is useful in standard type inference and gives expressive type-based program analyses, but raises difficult algorithmic problems. In a program analysis context we show how Mycroft's iterative method of computing principal types for a type system with polymorphic recursion can be generalized and adapted to work in a setting with subtyping. This does not only yield a proof of existence of principal types (most general properties), but also an algorithm for computing them. The punch-line of the development is that a very simple modification of the basic algorithm reduces its computational complexity from exponential time to polynomial time relative to the size of the given, explicitly typed program. This solves the open problem of finding an inference algorithm for polymorphic binding-time analysis
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/dussart1995.pdf
%8 September
%D 1995
%K parametricity