Soundness of Coercion in the Calculus of Constructions

DOI10.1093/LOGCOM/14.3.405zbMATH Open1060.03031OpenAlexW1970925243MaRDI QIDQ4820474FDOQ4820474

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

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

zbMATH Keywords

subtypingcoercioncalculus of constructions

Mathematics Subject Classification ID

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

Cited In (6)

• System F with coercion constraints
• Pure type systems with judgemental equality
• Title not available (Why is that?)
• Coercion completion and conservativity in coercive subtyping
• On the power of coercion abstraction
• Coercive subtyping for the calculus of constructions (extended abstract)

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)