Soundness of Coercion in the Calculus of Constructions

DOI10.1093/LOGCOM/14.3.405MaRDI QIDQ4820474zbMATH OpenOpenAlexFDO

Authors Gang Chen

Publication date 15 October 2004

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/14.3.405

zbMATH Keywords

subtypingcoercioncalculus of constructions

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Recommendations

• Coercive subtyping for the calculus of constructions (extended abstract)
• scientific article; zbMATH DE number 1086673
• Coercion completion and conservativity in coercive subtyping
• Coherence and Transitivity in Coercive Subtyping
• Coercive subtyping: theory and implementation

Cited in

(6)

• System F with coercion constraints
• Pure type systems with judgemental equality
• scientific article; zbMATH DE number 2185708 (Why is no real title available?)
• Coercion completion and conservativity in coercive subtyping
• On the power of coercion abstraction
• Coercive subtyping for the calculus of constructions (extended abstract)

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Soundness of Coercion in the Calculus of Constructions

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