Completeness and soundness results for X with intersection and union types

DOI10.3233/FI-2012-770MaRDI QIDQ4903713zbMATH OpenOpenAlexFDO

Authors Steffen Van Bakel

Publication date 24 January 2013

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2012-770

zbMATH Keywords

classical logicintersection typessequent calculusunion types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Intersection and union types for \(\mathcal{X}\)
• Intersection and union types: Syntax and semantics
• Sound and complete typing for \(\lambda\mu\)
• Completeness of intersection and union type assignment systems for call-by-value -models

Cited in

(11)

• Intersection and union types: Syntax and semantics
• Intersection and union types for \(\mathcal{X}\)
• Soundness and principal contexts for a shallow polymorphic type system based on classical logic
• Semantic types and approximation for Featherweight Java
• Sound and complete typing for \(\lambda\mu\)
• The duality of classical intersection and union types
• Functional type assignment for Featherweight Java. To Rinus Plasmeijer, in honour of his 61st birthday
• Completeness of intersection and union type assignment systems for call-by-value -models
• Completeness of type assignment systems with intersection, union, and type quantifiers
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• A completeness result for a realisability semantics for an intersection type system

This page was built for publication: Completeness and soundness results for \(\mathcal X\) with intersection and union types

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