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]

Authors

Inmaculada Medina-Bulo

This author has not been identified. Look up 'Inmaculada Medina-Bulo' in Google

Francisco Palomo-Lozano

This author has not been identified. Look up 'Francisco Palomo-Lozano' in Google

José-Luis Ruiz-Reina

This author has not been identified. Look up 'José-Luis Ruiz-Reina' in Google