ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System

Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina. ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. In Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt, editors, Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings. Volume 5625 of Lecture Notes in Computer Science, pages 106-121, Springer, 2009. [doi]

Authors

Francisco-Jesús Martín-Mateos

This author has not been identified. Look up 'Francisco-Jesús Martín-Mateos' in Google

Julio Rubio

This author has not been identified. Look up 'Julio Rubio' in Google

José-Luis Ruiz-Reina

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