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