Domain theoretic models of polymorphism

DOI10.1016/0890-5401(89)90068-0MaRDI QIDQ1824612zbMATH OpenOpenAlexFDO

Authors Thierry Coquand, Glynn Winskel, Carl A. Gunter

Publication date 1989

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

Full work available at URL https://doi.org/10.1016/0890-5401(89)90068-0

zbMATH Keywords

category-theoretic model for polymorphic lambda- calculuscontinuous sectionsGrothendieck fibrationsindexed categorypolymorphismScott domains

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Preorders, orders, domains and lattices (viewed as categories) (18B35) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The authors present a category-theoretic model for polymorphic lambda- calculus. Types are interpreted as Scott domains and types with free type variables as functors on domains. The paper emphasizes the important role Grothendieck fibrations and continuous sections play in the interpretation of polymorphism. The approach is based on examples, many particular constructions are presented so that the ideas are concretely expressed. Finally, the paper presents interesting questions and comparisons with other models for polymorphism.

Recommendations

• scientific article; zbMATH DE number 4027427
• scientific article; zbMATH DE number 517052
• scientific article; zbMATH DE number 937388
• Domain-theoretical models of parametric polymorphism
• scientific article; zbMATH DE number 4027428

Cites work

• An ideal model for recursive polymorphic types
• Effectively given domains
• scientific article; zbMATH DE number 3882403 (Why is no real title available?)
• scientific article; zbMATH DE number 3882404 (Why is no real title available?)
• scientific article; zbMATH DE number 3858394 (Why is no real title available?)
• scientific article; zbMATH DE number 3825806 (Why is no real title available?)
• scientific article; zbMATH DE number 4027427 (Why is no real title available?)
• scientific article; zbMATH DE number 4047723 (Why is no real title available?)
• scientific article; zbMATH DE number 4049849 (Why is no real title available?)
• scientific article; zbMATH DE number 4050971 (Why is no real title available?)
• scientific article; zbMATH DE number 3780545 (Why is no real title available?)
• scientific article; zbMATH DE number 3783068 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 3594646 (Why is no real title available?)
• The Category-Theoretic Solution of Recursive Domain Equations
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• The largest Cartesian closed category of domains
• The system \({\mathcal F}\) of variable types, fifteen years later
• Universal profinite domains

Cited in

(45)

• Recursion over realizability structures
• Inheritance as implicit coercion
• Quantitative domains and infinitary algebras
• Categorical models of polymorphism
• Some economic applications of Scott domains
• On functors expressible in the polymorphic typed lambda calculus
• Historical introduction to ``Concrete domains by G. Kahn and G. D. Plotkin
• A natural semantics of first-order type dependency
• Term graph rewriting and garbage collection using opfibrations
• Adequacy for a lazy functional language with recursive and polymorphic types
• A domain-theoretic semantics of lax generic functions.
• Polymorphic lambda calculus and subtyping.
• Building continuous webbed models for system F
• A full continuous model of polymorphism
• An adequacy theorem for dependent type theory
• Domain-theoretical models of parametric polymorphism
• A higher-order calculus and theory abstraction
• The dependent product construction in various categories of domains
• From parametric polymorphism to models of polymorphic FPC
• scientific article; zbMATH DE number 4154448 (Why is no real title available?)
• Some reasons for generalising domain theory
• Interpreting Polymorphic FPC into Domain Theoretic Models of Parametric Polymorphism
• scientific article; zbMATH DE number 4027427 (Why is no real title available?)
• scientific article; zbMATH DE number 4035777 (Why is no real title available?)
• scientific article; zbMATH DE number 4050971 (Why is no real title available?)
• Semantics of the second order lambda calculus
• The shuffle Hopf algebra and noncommutative full completeness
• scientific article; zbMATH DE number 517052 (Why is no real title available?)
• Categorical data types in parametric polymorphism
• scientific article; zbMATH DE number 1497800 (Why is no real title available?)
• scientific article; zbMATH DE number 1531357 (Why is no real title available?)
• Polymorphism and the obstinate circularity of second order logic: a victims' tale
• scientific article; zbMATH DE number 2102746 (Why is no real title available?)
• Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi
• Parametricity of extensionally collapsed term models of polymorphism and their categorical properties
• Models for polymorphism over physical dimension
• Computer Science Logic
• Types, abstraction, and parametric polymorphism, part 2
• Extensional models for polymorphism
• The semantics of second-order lambda calculus
• Functorial polymorphism
• Alpha conversion, conditions on variables and categorical logic
• Domain interpretations of Martin-Löf's partial type theory
• An algebraic approach to stable domains
• A domain model characterising strong normalisation

This page was built for publication: Domain theoretic models of polymorphism

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