A sort parametric polymorphism for algebraic specifications

We propose to extend the standard algebraic specification framework by incorporating user-defined type constructors that accept types and data as arguments. Together with the concept of term construction, this enhancement provides a powerful type system that includes parametric polymorphism and dependent types. Typing restrictions are specified by a small set of axioms and deduction rules. A type-checking algorithm is developed and proven to be sound with respect to the typing rules. This work has been developed in the framework of the specification language SEGRAS.