A verified Common Lisp implementation of Buchberger’s algorithm in ACL2 | Publicación