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

DOI10.1145/1391289.1391293MaRDI QIDQ3452185zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

higher-order functionsintersection typesnegation typessubtypingunion types

Mathematics Subject Classification ID

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

Recommendations

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

Cited in

(30)

• Subtyping can have a simple semantics
• Backward type inference for XML queries
• Precise subtyping for synchronous multiparty sessions
• Judgmental subtyping systems with intersection types and modal types
• The relevance of semantic subtyping
• The better bubbling lemma
• On projecting processes into session types
• Semantic subtyping with an SMT solver
• Sound and complete flow typing with unions, intersections and negations
• The recursive union of some gradual types
• scientific article; zbMATH DE number 1479640 (Why is no real title available?)
• scientific article; zbMATH DE number 7453961 (Why is no real title available?)
• Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types
• The -calculus: syntax and types
• Semantic subtyping for non-strict languages
• Type Inference for Rank 2 Gradual Intersection Types
• Semantic subtyping with an SMT solver
• scientific article; zbMATH DE number 7168151 (Why is no real title available?)
• Computer Science Logic
• Theoretical Computer Science
• Automata, Languages and Programming
• Precise Subtyping for Asynchronous Multiparty Sessions
• Automated Deduction – CADE-19
• Polarized subtyping
• Applicative intersection types
• A calculus with recursive types, record concatenation and subtyping
• Categorical approximation fixpoint theory
• On specifications, subset types and interpretation of proposition in type theory
• Inference systems with corules for fair subtyping and liveness properties of binary session types
• A typed lambda calculus with intersection types

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)