Details:
Title  Gröbner Bases in Type Theory  Author(s)  Thierry Coquand, Henrik Persson  Type  Book, Chapter in Book, Conference Proceeding  Abstract  We describe how the theory of Groebner bases, an important part of
computational algebra, can be developed within MartinLöf's type
theory. In particular, we aim for an integrated development of the
algorithms for computing Groebner bases: we want to prove,
constructively in type theory, the existence of Groebner bases and
from such proofs extract the algorithms. Our main contribution is a
reformulation of the standard theory of Grobner bases which uses
generalised inductive definitions. We isolate the main
nonconstructive part, a minimal bad sequence argument, and use the
open induction principle [Rao88, Coq92] to interpret it by induction.
This leads to short constructive proofs of Dickson's lemma and
Hilbert's basis theorem, which are used to give an integrated
development of Buchberger's algorithm. An important point of this
work is that the elegance and brevity of the original proofs are
maintained while the new proofs also have a direct constructive
content. In the appendix we present a computer formalisation of Dickson's lemma and an abstract existence proof of Groebner bases. 
Language  English  Journal  Lectures Notes in Computer Science  Volume  1657  Pages  p. 33  Publisher  SpringerVerlag GmbH  Year  1999  Editor  T. Altenkirch, W. Naraschewski, B. Reus  Edition  0  Translation 
No  Refereed 
No  Book  Types for Proofs and Programs: International Workshop, TYPES '98 
