Coercive subtyping for the calculus of constructions

DOI10.1145/604131.604145zbMath1321.68143OpenAlexW2074513246MaRDI QIDQ2942921

Gang Chen

Publication date: 11 September 2015

Published in: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

calculus of constructionssubtypingcoercionsemantics of coercionstransitivity elimination

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ Working with Mathematical Structures in Type Theory

Uses Software

• TREX

Cites Work

• Regular expression pattern matching for XML
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Coercive subtyping for the calculus of constructions