Exploring Abstract Algebra in Constructive Type Theory
unofficial copies [PDF], [PS]


by Paul B. Jackson

Proceedings of 12th Conference on Automated Deduction, A. Bundy (ed.), Springer-Verlag:NY, 1994.

Abstract

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.