An ideal model for recursive polymorphic types

DOI10.1016/S0019-9958(86)80019-5MaRDI QIDQ3776602zbMATH OpenOpenAlexFDO

Authors Ravi Sethi, David MacQueen, Gordon D. Plotkin

Publication date 1986

Published in Information and Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0019-9958(86)80019-5

zbMATH Keywords

fixed pointsdomainsrecursive typescomplete partial orderspolymorphic typesmetric space of idealssemantics of type expressionstype-inference rules

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) Model theory (03C99)

Recommendations

• Semantic types: a fresh look at the ideal model for types
• FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES
• scientific article; zbMATH DE number 4180813
• scientific article; zbMATH DE number 4126291
• Topological Completeness in an Ideal Model for Polymorphic Types

Cited in

(50)

• Type classes with existential types
• Contractive signatures with recursive types, type parameters, and abstract types
• Type inference with recursive types: Syntax and semantics
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Filter models with polymorphic types
• A record calculus with principal types
• Singleton, union and intersection types for program extraction
• A coinductive completeness proof for the equivalence of recursive types
• Topological Completeness in an Ideal Model for Polymorphic Types
• Type inference, abstract interpretation and strictness analysis
• scientific article; zbMATH DE number 2112161 (Why is no real title available?)
• Semantics of the second order lambda calculus
• scientific article; zbMATH DE number 4180813 (Why is no real title available?)
• Type inference with simple subtypes
• Polymorphic lambda calculus and subtyping.
• A semantics of multiple inheritance
• scientific article; zbMATH DE number 2102746 (Why is no real title available?)
• Logic of subtyping
• Elaborating intersection and union types
• Categorical models for non-extensional λ-calculi and combinatory logic
• Polymorphic type inference and containment
• Simplifying subtyping constraints: a theory
• Recursion over realizability structures
• The semantics of second-order lambda calculus
• Combining type disciplines
• Semantic types: a fresh look at the ideal model for types
• scientific article; zbMATH DE number 3938562 (Why is no real title available?)
• Recursive types for Fun
• Intersection and union types
• A realizability interpretation for intersection and union types
• Meta-circular interpreter for a strongly typed language
• Realisability semantics of parametric polymorphism, general references and recursive types
• An introduction to metric semantics: Operational and denotational models for programming and specification languages
• Pebble, a kernel language for modules and abstract data types
• Toward a semantics for the QUEST language
• Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models
• Modelling multiple inheritance with colimits
• Adequacy for a lazy functional language with recursive and polymorphic types
• Completeness of type assignment systems with intersection, union, and type quantifiers
• Subtyping constrained types
• Domain theoretic models of polymorphism
• Labelled reductions, runtime errors, and operational subsumption
• Syntactic soundness proof of a type-and-capability system with hidden state
• Isomorphism of intersection and union types
• Intuitionistic fixed point logic
• FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES
• Programming Languages and Systems
• The ``relevance of intersection and union types
• Bunched polymorphism
• Baby Modula-3 and a theory of objects

Describes a project that uses

Uses Software

• LCF

This page was built for publication: An ideal model for recursive polymorphic types

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