{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T18:02:08Z","timestamp":1745172128316,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_23","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"354-370","source":"Crossref","is-referenced-by-count":2,"title":["Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms"],"prefix":"10.1007","author":[{"given":"Laureano","family":"Lamb\u00e1n","sequence":"first","affiliation":[]},{"given":"Francisco J.","family":"Mart\u00edn-Mateos","sequence":"additional","affiliation":[]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9-Luis","family":"Ruiz-Reina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"ACL2 version 7.4. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/"},{"issue":"9","key":"23_CR2","first-page":"1","volume":"25","author":"J Aransay","year":"2015","unstructured":"Aransay, J., Divas\u00f3n, J.: Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm. J. Funct. Program. 25(9), 1\u201321 (2015)","journal-title":"J. Funct. Program."},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"1005","DOI":"10.1007\/s00165-016-0383-1","volume":"28","author":"J Aransay","year":"2016","unstructured":"Aransay, J., Divas\u00f3n, J.: Formalization of the computation of the echelon form of a matrix in Isabelle\/HOL. Form. Asp. Comput. 28, 1005\u20131026 (2016)","journal-title":"Form. Asp. Comput."},{"issue":"2","key":"23_CR4","first-page":"1","volume":"12","author":"G Cano","year":"2016","unstructured":"Cano, G., Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: Formalized linear algebra over elementary divisor rings in Coq logical methods in computer. Science 12(2), 1\u201329 (2016)","journal-title":"Science"},{"key":"23_CR5","unstructured":"Cowles, J., Gamboa, R., Van Baalen, J.: Using ACL2 arrays to formalize matrix algebra. In: Proceedings of ACL2 2003 (2003)"},{"key":"23_CR6","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1287\/moor.12.1.50","volume":"12","author":"PD Domich","year":"1987","unstructured":"Domich, P.D., Kannan, R., Trotter Jr., L.E.: Hermite normal form computation using modulo determinant arithmetic. Math. Oper. Res. 12, 50\u201369 (1987)","journal-title":"Math. Oper. Res."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Goel, S., Hunt Jr., W.A., Kaufmann, M.: Abstract stobjs and their application to ISA modeling. In: Proceedings of ACL2 2013, pp. 54\u201369 (2013)","DOI":"10.4204\/EPTCS.114.5"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-22863-6_10","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2011","unstructured":"Gonthier, G.: Point-free, set-free concrete linear algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 103\u2013118. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22863-6_10"},{"issue":"4","key":"23_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2528929","volume":"14","author":"J Heras","year":"2013","unstructured":"Heras, J., Coquand, T., M\u00f6rtberg, A., Siles, V.: Computing persistent homology within Coq\/SSReflect. ACM Trans. Comput. Log. 14(4), 1\u201326 (2013)","journal-title":"ACM Trans. Comput. Log."},{"key":"23_CR10","unstructured":"Lamb\u00e1n, L., Mart\u00edn-Mateos, F.-J., Rubio, J., Ruiz-Reina, J.-L.: Towards a verifiable topology of data. In: Proceedings of EACA-2016, pp. 113\u2013116 (2016)"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/S0024-3795(96)00163-2","volume":"254","author":"M Newman","year":"1997","unstructured":"Newman, M.: The Smith normal form. Linear Algebra Appl. 254, 367\u2013381 (1997)","journal-title":"Linear Algebra Appl."},{"key":"23_CR12","unstructured":"Storjohann, A.: Algorithms for matrix canonical forms. Ph.D. thesis, Swiss Federal Institute of Technology, Zurich (2013)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:08:05Z","timestamp":1664431685000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}