Type inference with simple subtypes

DOI10.1017/S0956796800000113zbMath0941.68541MaRDI QIDQ4939703

John C. Mitchell

Publication date: 9 February 2000

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

polymorphismfunctional programminglambda calculussubtypestype inference algorithms

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Related Items

Type reconstruction with recursive types and atomic subtyping ⋮ Reduction and unification in lambda calculi with a general notion of subtype ⋮ Non-structural subtype entailment in automata theory ⋮ Strong normalization for non-structural subtyping via saturated sets ⋮ Type inference with non-structural subtyping ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ Constraints for polymorphic behaviours of concurrent ML ⋮ Encoding natural semantics in Coq ⋮ Strong normalization with non-structural subtyping ⋮ Transitivity in coercive subtyping ⋮ Unnamed Item ⋮ A descriptive type foundation for RDF Schema ⋮ Some complexity bounds for subtype inequalities ⋮ Subtyping constrained types

Cites Work

• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A semantics of multiple inheritance
• Polymorphic type inference and containment
• On the semantics of polymorphism
• The completeness theorem for typing lambda-terms
• Curry's type-rules are complete with respect to the F-semantics too
• A filter lambda model and the completeness of type assignment
• On the sequential nature of unification
• An ideal model for recursive polymorphic types
• The Category-Theoretic Solution of Recursive Domain Equations
• Data Types as Lattices
• What is a model of the lambda calculus?
• A Machine-Oriented Logic Based on the Resolution Principle
• The Principal Type-Scheme of an Object in Combinatory Logic