Abstract for:
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 describe my implementation of computational abstract algebra in
the Nuprl system. I focus on my development of multivariate
polynomials. I show how I use Nuprl's expressive type theory to
define classes of free abelian monoids and free monoid algebras. These
classes are combined to create a class of all implementations of
polynomials.
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.
Last Modified Sep 18th, 1996