Paul B. Jackson. Exploring Abstract Algebra in Constructive Type Theory. In A. Bundy, editor, 12th International Conference on Automated Deduction, Lecture Notes in Artifical Intelligence. Springer Verlag, June 1994.
I discuss the issues of subtyping and computational content that came up in designing the class definitions. I give examples of relevant theory developments, tactics and proofs. I consider how Nuprl could act as an algebraic `oracle' for a computer algebra system and the relevance of this work for abstract functional programming.