Soundness of Coercion in the Calculus of Constructions

DOI10.1093/LOGCOM/14.3.405zbMath1060.03031OpenAlexW1970925243MaRDI QIDQ4820474

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

calculus of constructionssubtypingcoercion

Mathematics Subject Classification ID

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

Uses Software

• Automath

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