An Integrated Development of Buchberger's Algorithm in Coq
Henrik Persson · OpenGrey (Institut de l'Information Scientifique et Technique) · 2001
We present an integrated formal development of Buchberger's algorithm in Coq, that is we prove constructively the existence of Gröbner bases without explicitly writing the algorithm. This formalisation is based on an external formalisation in Coq by Théry, and an integrated abstract development in Agda. We end by discussing some experiences and differences between the two proof-styles and theorem-provers. This report was completed in March 2000.