Dirk Dussart, Fritz Henglein, Christian Mossin. Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time. In Proc.\ 2nd Int'l Static Analysis Symposium (SAS), Glasgow, Scotland, Lecture Notes in Computer Science, Pages 118-135, September 1995.
Download paper:
Adobe portable document (pdf)
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
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
[ sas95 ]
[ Parametricity ]
Dirk Dussart
Fritz Henglein
Christian Mossin
@InProceedings{dhm95b,
Author = {Dussart, Dirk and Henglein, Fritz and Mossin, Christian},
Title = {Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time},
BookTitle = {Proc.\ 2nd Int'l Static Analysis Symposium (SAS), Glasgow, Scotland},
Pages = {118--135},
Series = {Lecture Notes in Computer Science},
Publisher = {Springer-Verlag},
Month = {September},
Year = {1995}
}
Get EndNote Reference (.ref)