http:^^www.cs.cornell.edu^info^people^jackson^papers^ab-alg-abstract.html

This data set contains WWW-pages collected from computer science departments of various universities

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

<title>Abstract of Algebra / Type Theory CADE94 Paper</title>

Abstract for: <br>
Paul B. Jackson. Exploring Abstract Algebra in Constructive Type Theory.  In A.
Bundy, editor, <cite>12th International Conference on Automated
Deduction,</cite> Lecture Notes in Artifical Intelligence. Springer
Verlag, June 1994.  <p>

<hr>

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. 
<p>
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.
<p>

<hr>
Last Modified Jan 20th, 1995<p>

<address> Paul Jackson / <a href="mailto:[e-mail]">[e-mail]</a> </address>