Polymorphic type inference and containment

DOI10.1016/0890-5401(88)90009-0MaRDI QIDQ1110312zbMATHOpenAlexFDO

Authors John 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) Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65)

Recommendations

• Type inference in polymorphic type discipline
• scientific article; zbMATH DE number 3930968
• Polymorphic type inference with overloading and subtyping
• Type inference for polymorphic references
• Polymorphic typed defunctionalization and concretization
• Polymorphic typed defunctionalization
• scientific article; zbMATH DE number 3881858
• Flexible types, robust type inference for first-class polymorphism
• scientific article; zbMATH DE number 7577586
• Intensional polymorphism in type-erasure semantics

Cites work

• scientific article; zbMATH DE number 3880074 (Why is no real title available?)
• scientific article; zbMATH DE number 3928328 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 3360145 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
• A filter lambda model and the completeness of type assignment
• A theory of type polymorphism in programming
• An ideal model for recursive polymorphic types
• Combinatory logic. With two sections by William Craig.
• Completeness in the theory of types
• Curry's type-rules are complete with respect to the F-semantics too
• Data Types as Lattices
• Edinburgh LCF. A mechanized logic of computation
• Effective operations on partial recursive functions
• Linear unification
• On the Semantics of “Data Type”
• The Expressiveness of Simple and Second-Order Type Structures
• The Principal Type-Scheme of an Object in Combinatory Logic
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• The completeness theorem for typing lambda-terms
• The lambda calculus. Its syntax and semantics. Rev. ed.
• What is a model of the lambda calculus?

Cited in

(56)

• Types as parameters
• Programming Languages and Systems
• Signature restriction for polymorphic algebraic effects
• On the building of affine retractions
• Typability and type checking in System F are equivalent and undecidable
• Type inference with recursive types: Syntax and semantics
• Completeness of type assignment systems with intersection, union, and type quantifiers
• Semantics of the second order lambda calculus
• System ST toward a type system for extraction and proofs of programs
• Type inference with simple subtypes
• Complete restrictions of the intersection type discipline
• Intersection type assignment systems
• Type-directed bounding of collections in reactive programs
• Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models
• Basic polymorphic typechecking
• A modest model of records, inheritance, and bounded quantification
• scientific article; zbMATH DE number 773983 (Why is no real title available?)
• Intensional polymorphism in type-erasure semantics
• scientific article; zbMATH DE number 4014021 (Why is no real title available?)
• A Polymorphic Type System for the Lambda-Calculus with Constructors
• A Church-style intermediate language for ML\(^{\text F}\)
• Recasting ML\(^{\text F}\)
• Constructive natural deduction and its ‘ω-set’ interpretation
• Type reconstruction in finite rank fragments of the second-order \(\lambda\)-calculus
• scientific article; zbMATH DE number 7577586 (Why is no real title available?)
• scientific article; zbMATH DE number 3930968 (Why is no real title available?)
• \(F\)-semantics for type assignment systems
• The semantics of second-order lambda calculus
• The relevance of semantic subtyping
• Recursion over realizability structures
• A semantic basis for Quest
• A System F with Call-by-Name Exceptions
• Nominalization, predication and type containment
• Typed equivalence, type assignment, and type containment
• Strong normalization for non-structural subtyping via saturated sets
• A sequent calculus for subtyping polymorphic types
• Logic of subtyping
• The subtyping problem for second-order types is undecidable.
• Complete types in an extension of the system \({\mathcal A}{\mathcal F}2\)
• Recursive types for Fun
• Type inference, abstract interpretation and strictness analysis
• Fully abstract submodels of typed lambda calculi
• Type soundness for path polymorphism
• Syntactic soundness proof of a type-and-capability system with hidden state
• Polytypic values possess polykinded types
• Polymorphic type inference for the relational algebra
• A paradigmatic object-oriented programming language: Design, static typing and semantics
• A semantics for type checking
• Domain-free \(\lambda\mu\)-calculus
• A language for generic programming in the large
• Filter models with polymorphic types
• Intersection, Universally Quantified, and Reference Types
• Generalized filter models
• Corrigendum: Polymorphic type assignment and CPS conversion
• scientific article; zbMATH DE number 1487941 (Why is no real title available?)
• Type inference in polymorphic type discipline

Describes a project that uses

Uses Software

• ML

This page was built for publication: Polymorphic type inference and containment

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1110312)