A Logical Approach to Deciding Semantic Subtyping

We consider a type algebra equipped with recursive, product, function, intersection, union, and complement types, together with type variables. We consider the subtyping relation defined by Castagn...