An algebraic semantics of higher-order types with subtypes
This paper extends order-sorted algebras with higher-order functions
for functional programming, data type specification and
The main results are a new subtype relation,
a new semantics for higher-order order-sorted types and a new
complete equational deduction calculus.