| A Semantics for Static Type Inference (1991). A-SEMANTICS FOR TYPE CHECKING | |||||||||||||
Abstract | |||||||||||||
| Curry’s system for F-deducibility is the basis for static type inference algorithms for programming languages such as ML. If a natural “preservation of types by conversion” rule is added to Curry’s system, it becomes undecidable, but complete relative to a variety of model classes. We show completeness for Curry’s system itself, relative to an extended notion of model that validates reduction but not conversion. Two proofs are given: one uses a term model and the other a model built from type expressions. Extensions to systems with polymorphic or intersection types are also considered. | |||||||||||||
Publication details | |||||||||||||
| |||||||||||||
Cited publications (1) | |||||||||||||
| |||||||||||||