Abstract
We give a purely syntactic proof (from scratch) of the subject equality property of the BCD intersection type system through a reformulation of the subtyping relation having a “cut-elimination” property.
Get full access to this article
View all access options for this article.