A verified Common Lisp implementation of Buchberger’s algorithm in ACL2 - Medina-Bulo, Inmaculada; Palomo-Lozano, Francisco; Ruiz-Reina, José-Luis (Journal of Symbolic Computation, 2010)