Provable computable functions on abstract data types

We work in the context of abstract data types, modelled as classes of many-sorted algebras. We develop notions of computability over such data types, in particular notions of primitive recursiveness and μ-recursiveness, which generalize the corresponding classical notions over the natural numbers. We also develop classical and intuitionistic formal systems for theories over such data types, and prove (in the case of universal theories) that if …