An algebraic semantics of higher-order types with subtypes

Abstract:

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

For a preprint send a message to Zhenyu Qian.