Sound and complete elimination of singleton kinds

DOI10.1145/1227839.1227840MaRDI QIDQ5277773zbMATH OpenOpenAlexFDO

Authors Karl Crary

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

singleton kindstype systems

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• scientific article; zbMATH DE number 1746455
• Deciding type equivalence in a language with singleton kinds
• Strong normalization with singleton types
• Extensional equivalence and singleton types
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

Cited in

(3)

• scientific article; zbMATH DE number 1746455 (Why is no real title available?)
• Deciding type equivalence in a language with singleton kinds
• Dynamic translucency with abstraction kinds and higher-order coercions

This page was built for publication: Sound and complete elimination of singleton kinds

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