A verified Common Lisp implementation of Buchberger s algorithm in ACL2

Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José-Luis Ruiz-Reina. A verified Common Lisp implementation of Buchberger s algorithm in ACL2. Journal of Symbolic Computation, 45(1):96-123, 2010. [doi]