Domain theoretic models of polymorphism

DOI10.1016/0890-5401(89)90068-0zbMath0683.03007OpenAlexW2131781021MaRDI QIDQ1824612

Glynn Winskel, Thierry Coquand, 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

polymorphismScott domainsindexed categorycontinuous sectionscategory-theoretic model for polymorphic lambda- calculusGrothendieck fibrations

Mathematics Subject Classification ID

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

Related Items (27)

The shuffle Hopf algebra and noncommutative full completeness ⋮ Term graph rewriting and garbage collection using opfibrations ⋮ Adequacy for a lazy functional language with recursive and polymorphic types ⋮ A higher-order calculus and theory abstraction ⋮ The dependent product construction in various categories of domains ⋮ Categorical data types in parametric polymorphism ⋮ Semantics of the second order lambda calculus ⋮ Parametricity of extensionally collapsed term models of polymorphism and their categorical properties ⋮ Types, abstraction, and parametric polymorphism, part 2 ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ Domain interpretations of Martin-Löf's partial type theory ⋮ An algebraic approach to stable domains ⋮ Recursion over realizability structures ⋮ Inheritance as implicit coercion ⋮ Quantitative domains and infinitary algebras ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ Some reasons for generalising domain theory ⋮ Some economic applications of Scott domains ⋮ The semantics of second-order lambda calculus ⋮ Functorial polymorphism ⋮ An adequacy theorem for dependent type theory ⋮ Unnamed Item ⋮ Building continuous webbed models for system F ⋮ A full continuous model of polymorphism ⋮ Historical introduction to ``Concrete domains by G. Kahn and G. D. Plotkin ⋮ A natural semantics of first-order type dependency ⋮ Polymorphic lambda calculus and subtyping.

Cites Work

• The largest Cartesian closed category of domains
• The system \({\mathcal F}\) of variable types, fifteen years later
• Universal profinite domains
• Effectively given domains
• An ideal model for recursive polymorphic types
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• The Category-Theoretic Solution of Recursive Domain Equations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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