Polymorphic type inference and containment

DOI10.1016/0890-5401(88)90009-0zbMATH Open0656.68023OpenAlexW2080040385MaRDI QIDQ1110312FDOQ1110312

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

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

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)

Cites Work

• A theory of type polymorphism in programming
• Edinburgh LCF. A mechanized logic of computation
• On the Semantics of “Data Type”
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Data Types as Lattices
• Linear unification
• A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
• A Machine-Oriented Logic Based on the Resolution Principle
• A filter lambda model and the completeness of type assignment
• Completeness in the theory of types
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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 Expressiveness of Simple and Second-Order Type Structures
• The completeness theorem for typing lambda-terms
• Effective operations on partial recursive functions
• What is a model of the lambda calculus?
• Title not available (Why is that?)
• Curry's type-rules are complete with respect to the F-semantics too
• Title not available (Why is that?)
• An ideal model for recursive polymorphic types
• Title not available (Why is that?)

Cited In (56)

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

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)