Using abstract stobjs in ACL2 to compute matrix normal forms
scientific article; zbMATH DE number 6821862