Anzeige
Erschienen in:
1991 | ReviewPaper | Buchkapitel
A semantics for type checking
verfasst von : Gordon Plotkin
Erschienen in: Theoretical Aspects of Computer Software
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Curry's system for F-deducibility is the basis for implicit type checking for programming languages such as ML. If a natural “preservation of types by conversion” rule is added it becomes undecidable, but complete relative to a variety of model classes. We show completeness for F-deducibility itself, relative to an extended notion of model which validates reduction but not conversion. Both term model and filter model proofs are given, and the extension to polymorphic typing is also considered.