Polymorphic type inference and containment
type: Item
instance of: scholarly article
title: Polymorphic type inference and containment
zbMATH Open document ID: 0656.68023
DOI: 10.1016/0890-5401(88)90009-0
author: John Mitchell
published in: Information and Computation
publication date: 1988-01-01T00:00:00Z
review text: Type expressions may be used to describe the functional behaviour of untyped lambda terms. A semantics for quantified types over arbitrary models of untyped lambda calculus is presented. Completeness theorems for inference models without empty types, simple inference models, quotient- set semantics of types as well as for models that may have empty types are proven. Containment relation on types is used to get some insight into the set of quantified types associated with a term. To that end containments that hold in all semantic models are investigated using a pure type assignment system based on containment.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 4072356
zbMATH Keywords: type expressions
zbMATH Keywords: lambda models
zbMATH Keywords: quantified types
zbMATH Keywords: containment
reviewed by: Luboš Brim
describes a project that uses: ML
MaRDI profile type: Publication
full work available at URL: 0890-5401(88)90009-0
OpenAlex ID: W2080040385
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: A filter lambda model and the completeness of type assignment
cites work: Combinatory logic. With two sections by William Craig.
cites work: Q3345747
cites work: On the Semantics of “Data Type”
cites work: The Expressiveness of Simple and Second-Order Type Structures
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Completeness in the theory of types
cites work: The Principal Type-Scheme of an Object in Combinatory Logic
cites work: The completeness theorem for typing lambda-terms
cites work: Curry's type-rules are complete with respect to the F-semantics too
cites work: A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
cites work: Q5344164
cites work: An ideal model for recursive polymorphic types
cites work: Q3702495
cites work: What is a model of the lambda calculus?
cites work: A theory of type polymorphism in programming
cites work: Effective operations on partial recursive functions
cites work: Linear unification
cites work: Q4068054
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Data Types as Lattices
cites work: Q5633977
cites work: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
Recommended article: Type inference in polymorphic type discipline
Recommended article: Q3705422
Recommended article: Polymorphic type inference with overloading and subtyping
Recommended article: Type inference for polymorphic references
Recommended article: Polymorphic typed defunctionalization and concretization
Recommended article: Polymorphic typed defunctionalization
Recommended article: Q3216117
Recommended article: Flexible types
Recommended article: Q5101355
Recommended article: Intensional polymorphism in type-erasure semantics
description: scientific article; zbMATH DE number 4072356