Semantic subtyping

2008/09/01 by Alain Frisch, Giuseppe Castagna, Véronique Benzaken · 140 citations
Computer Science · #Abstract interpretation #Advanced Database Systems and Queries #Computer science #Data mining #Denotational semantics #Denotational semantics of the Actor model #Interpretation (philosophy) #Logic, programming, and type systems #Operational semantics #Programming language #Relation (database) #Semantic Web and Ontologies #Semantics (computer science) #Subtyping #Theoretical computer science

paper · doi:10.1145/1391289.1391293

published in Journal of the ACM 55(4), 1-64 (Association for Computing Machinery)

openalex publication_date 2008/09/01 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/01

Abstract

Subtyping relations are usually defined either syntactically by a formal system or semantically by an interpretation of types into an untyped denotational model. This work shows how to define a subtyping relation semantically in the presence of Boolean connectives, functional types and dynamic dispatch on types, without the complexity of denotational models, and how to derive a complete subtyping algorithm.

Cited by

• Programming with Union, Intersection, and Negation Types
• XTQ: A Declarative Functional XML Query Language
• Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
• Revisiting Elementary Denotational Semantics
• Set-Theoretic Types for Polymorphic Variants
• Can determinism and compositionality coexist in RML? (extended version)
• The Design Principles of the Elixir Type System
• Semantic Subtyping for Maps in Erlang
• JSON Schema Inclusion through Refutational Normalization: Reconciling Efficiency and Completeness
• Preciseness of Subtyping on Intersection and Union Types
• SFJ: An Implementation of Semantic Featherweight Java [europepmc]

Related

• Categorical models of subtyping
• Semantic Subtyping for Maps in Erlang
• A behavioral notion of subtyping
• Phantom Types and Subtyping
• Transitivity of Subtyping for Intersection Types