MIME-Version: 1.0 Server: CERN/3.0 Date: Sunday, 24-Nov-96 19:07:26 GMT Content-Type: text/html Content-Length: 1149 Last-Modified: Friday, 20-Jan-95 16:47:22 GMT Abstract of Algebra / Type Theory CADE94 Paper 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 Jan 20th, 1995

Paul Jackson / jackson@cs.cornell.edu