Typed compilation of inclusive subtyping

DOI10.1145/351240.351247MaRDI QIDQ2943358zbMATH OpenOpenAlexFDO

Authors Karl Crary

Publication date 11 September 2015

Published in Proceedings of the fifth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Coherence of subsumption for monadic types
• Foundations for the implementation of higher-order subtyping
• Optimal representations of polymorphic types with subtyping
• scientific article; zbMATH DE number 2086502
• Coercive subtyping

Cited in

(9)

• A Church-style intermediate language for ML\(^{\text F}\)
• scientific article; zbMATH DE number 2086494 (Why is no real title available?)
• scientific article; zbMATH DE number 2086502 (Why is no real title available?)
• Explicit effect subtyping
• Typed cross-module compilation
• Safe zero-cost coercions for Haskell
• Dynamic translucency with abstraction kinds and higher-order coercions
• 2-Dimensional Directed Type Theory
• Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions

This page was built for publication: Typed compilation of inclusive subtyping

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