An ideal model for recursive polymorphic types

DOI10.1016/S0019-9958(86)80019-5zbMATH Open0636.68016OpenAlexW2090415524MaRDI QIDQ3776602FDOQ3776602

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

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

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)

Cited In (50)

• Type classes with existential types
• Contractive signatures with recursive types, type parameters, and abstract types
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• A record calculus with principal types
• Singleton, union and intersection types for program extraction
• Type inference with recursive types: Syntax and semantics
• Topological Completeness in an Ideal Model for Polymorphic Types
• A coinductive completeness proof for the equivalence of recursive types
• Filter models with polymorphic types
• Type inference, abstract interpretation and strictness analysis
• Title not available (Why is that?)
• Semantics of the second order lambda calculus
• Title not available (Why is that?)
• Type inference with simple subtypes
• Polymorphic lambda calculus and subtyping.
• A semantics of multiple inheritance
• Title not available (Why is that?)
• 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
• The semantics of second-order lambda calculus
• Recursion over realizability structures
• Combining type disciplines
• Semantic types: a fresh look at the ideal model for types
• Title not available (Why is that?)
• Intersection and union types
• Recursive types for Fun
• A realizability interpretation for intersection and union types
• An introduction to metric semantics: Operational and denotational models for programming and specification languages
• Realisability semantics of parametric polymorphism, general references and recursive types
• Meta-circular interpreter for a strongly typed language
• Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models
• Toward a semantics for the QUEST language
• Pebble, a kernel language for modules and abstract data types
• Completeness of type assignment systems with intersection, union, and type quantifiers
• Modelling multiple inheritance with colimits
• Subtyping constrained types
• Adequacy for a lazy functional language with recursive and polymorphic 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
• Programming Languages and Systems
• Intuitionistic fixed point logic
• FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES
• The ``relevance of intersection and union types
• Bunched polymorphism
• Baby Modula-3 and a theory of objects

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)