Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms.

Laureano Lambn, Francisco J. Martn-Mateos, Julio Rubio, Jos-Luis Ruiz-Reina

Browse the full ITP paper archive.