Proof of the principal type property for system O
Abstract:
We study a minimal extension of the Hindley/Milner system that
supports overloading and polymorphic records.
We also show that every typable term in this system has a
principal type and give an algorithm to reconstruct that type.
We give the proofs for termination, soundness and correctness for
the constrained unification and the type reconstruction algorithm.
| Zugehörige Institution(en) am KIT | Institut für Programmstrukturen und Datenorganisation (IPD) |
| Publikationstyp | Buch |
| Publikationsjahr | 1996 |
| Sprache | Englisch |
| Identifikator | urn:nbn:de:swb:90-AAA179964 KITopen-ID: 17996 |
| Erscheinungsvermerk | Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,16.) |