Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types

DOI10.1145/1391289.1391293zbMATH Open1325.68136OpenAlexW1988897846MaRDI QIDQ3452185FDOQ3452185

Authors: Alain Frisch, Giuseppe Castagna, Véronique Benzaken 

Publication date: 11 November 2015

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1391289.1391293

Recommendations

• Automata, Languages and Programming
• Subtyping can have a simple semantics
• scientific article; zbMATH DE number 761284
• Theoretical Computer Science
• Computer Science Logic

zbMATH Keywords

subtypingintersection typeshigher-order functionsunion typesnegation types

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cited In (28)

• Title not available (Why is that?)
• A calculus with recursive types, record concatenation and subtyping
• Title not available (Why is that?)
• The relevance of semantic subtyping
• Precise subtyping for synchronous multiparty sessions
• The recursive union of some gradual types
• Automata, Languages and Programming
• Title not available (Why is that?)
• Polarized subtyping
• Title not available (Why is that?)
• Type Inference for Rank 2 Gradual Intersection Types
• Computer Science Logic
• Theoretical Computer Science
• Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types
• Automated Deduction – CADE-19
• On projecting processes into session types
• On specifications, subset types and interpretation of proposition in type theory
• Judgmental subtyping systems with intersection types and modal types
• Applicative intersection types
• Precise Subtyping for Asynchronous Multiparty Sessions
• Backward type inference for XML queries
• A typed lambda calculus with intersection types
• Title not available (Why is that?)
• Semantic subtyping with an SMT solver
• Semantic subtyping with an SMT solver
• The better bubbling lemma
• Categorical approximation fixpoint theory
• Sound and complete flow typing with unions, intersections and negations

This page was built for publication: Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types

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