Polymorphic type inference and containment

DOI10.1016/0890-5401(88)90009-0zbMath0656.68023OpenAlexW2080040385MaRDI QIDQ1110312

John C. Mitchell

Publication date: 1988

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(88)90009-0

zbMATH Keywords

containmentlambda modelsquantified typestype expressions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Combinatory logic and lambda calculus (03B40)

Related Items

Typed equivalence, type assignment, and type containment, \(F\)-semantics for type assignment systems, Types as parameters, Intersection type assignment systems, Strong normalization for non-structural subtyping via saturated sets, Constructive natural deduction and its ‘ω-set’ interpretation, Semantics of the second order lambda calculus, A semantics for type checking, Type inference in polymorphic type discipline, System ST toward a type system for extraction and proofs of programs, The subtyping problem for second-order types is undecidable., A Church-style intermediate language for ML\(^{\text F}\), A System F with Call-by-Name Exceptions, On the building of affine retractions, A modest model of records, inheritance, and bounded quantification, Recursion over realizability structures, Recursive types for Fun, Domain-Freeλµ-Calculus, Filter models with polymorphic types, Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus, Complete restrictions of the intersection type discipline, Syntactic soundness proof of a type-and-capability system with hidden state, A language for generic programming in the large, A semantic basis for Quest, Type inference with simple subtypes, Logic of subtyping, Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models, Completeness of type assignment systems with intersection, union, and type quantifiers, The semantics of second-order lambda calculus, A Polymorphic Type System for the Lambda-Calculus with Constructors, Recasting ML\(^{\text F}\), Type inference with recursive types: Syntax and semantics, Intersection, Universally Quantified, and Reference Types, Complete Types in an Extension of the System AF2, Generalized filter models, The Relevance of Semantic Subtyping, Typability and type checking in System F are equivalent and undecidable, A sequent calculus for subtyping polymorphic types, Nominalization, predication and type containment, Type inference, abstract interpretation and strictness analysis, A paradigmatic object-oriented programming language: Design, static typing and semantics

Uses Software

• ML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Linear unification
• A theory of type polymorphism in programming
• Edinburgh LCF. A mechanized logic of computation
• The completeness theorem for typing lambda-terms
• Curry's type-rules are complete with respect to the F-semantics too
• Effective operations on partial recursive functions
• A filter lambda model and the completeness of type assignment
• The Expressiveness of Simple and Second-Order Type Structures
• An ideal model for recursive polymorphic types
• On the Semantics of “Data Type”
• A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
• Data Types as Lattices
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• 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
• Completeness in the theory of types