{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:14:30Z","timestamp":1725988470053},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999562"},{"type":"electronic","value":"9783319999579"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99957-9_3","type":"book-chapter","created":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T04:26:31Z","timestamp":1534825591000},"page":"37-53","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Proof of the Computation of Hermite Normal Form in a General Setting"],"prefix":"10.1007","author":[{"given":"Jose","family":"Divas\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jes\u00fas","family":"Aransay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,22]]},"reference":[{"key":"3_CR1","unstructured":"Archive of Formal Proofs. \nhttp:\/\/afp.sourceforge.net\/"},{"key":"3_CR2","unstructured":"Immutable non-strict arrays in Haskell. \nhttp:\/\/hackage.haskell.org\/package\/array-0.5.2.0\/docs\/Data-Array.html"},{"key":"3_CR3","unstructured":"Matlab documentation. Definition of Hermite Normal Form. \nhttp:\/\/es.mathworks.com\/help\/symbolic\/hermiteform.html#butzrp_-5"},{"key":"3_CR4","unstructured":"The Vector structure in SML. \nhttp:\/\/sml-family.org\/Basis\/vector.html"},{"key":"3_CR5","unstructured":"HOL interactive theorem prover (2016). \nhttps:\/\/hol-theorem-prover.org\/"},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"22 p.","DOI":"10.1017\/S0956796815000155","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, 22 p. (2015). \nhttps:\/\/doi.org\/10.1017\/S0956796815000155","journal-title":"J. Funct. Program."},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/s10817-016-9379-z","volume":"58","author":"J Aransay","year":"2017","unstructured":"Aransay, J., Divas\u00f3n, J.: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem. J. Autom. Reason. 58, 509\u2013535 (2017). \nhttps:\/\/doi.org\/10.1007\/s10817-016-9379-z","journal-title":"J. Autom. Reason."},{"issue":"6","key":"3_CR8","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.: Formalisation of the computation of the echelon form of a matrix in Isabelle\/HOL. Formal Aspects Comput. 28(6), 1005\u20131026 (2016)","journal-title":"Formal Aspects Comput."},{"issue":"2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reason."},{"issue":"116","key":"3_CR10","doi-asserted-by":"publisher","first-page":"897","DOI":"10.1090\/S0025-5718-1971-0301909-X","volume":"25","author":"GH Bradley","year":"1971","unstructured":"Bradley, G.H.: Algorithms for Hermite and Smith normal matrices and linear diophantine equations. Math. Comput. 25(116), 897\u2013907 (1971)","journal-title":"Math. Comput."},{"key":"3_CR11","doi-asserted-by":"crossref","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 Comput. Sci. 12(2) (2016)","DOI":"10.2168\/LMCS-12(2:7)2016"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-03545-1_10","volume-title":"Certified Programs and Proofs","author":"C Cohen","year":"2013","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 147\u2013162. Springer, Cham (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-319-03545-1_10"},{"key":"3_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02945-9","volume-title":"A Course in Computational Algebraic Number Theory","author":"H Cohen","year":"1993","unstructured":"Cohen, H.: A Course in Computational Algebraic Number Theory. Springer, New York (1993). \nhttps:\/\/doi.org\/10.1007\/978-3-662-02945-9"},{"issue":"1","key":"3_CR14","first-page":"27","volume":"5","author":"T Coquand","year":"2012","unstructured":"Coquand, T., M\u00f6rtberg, A., Siles, V.: A formal proof of Sasaki-Murao algorithm. J. Formalized Reason. 5(1), 27\u201336 (2012)","journal-title":"J. Formalized Reason."},{"key":"3_CR15","unstructured":"The Coq development team. The Coq proof assistant reference manual. LogiCal Project (2018). Version 8.8.0. \nhttp:\/\/coq.inria.fr"},{"key":"3_CR16","unstructured":"Divas\u00f3n, J.: Additional files to the Hermite normal form development (2018). \nhttp:\/\/www.unirioja.es\/cu\/jodivaso\/Isabelle\/Hermite\/Hermite.html"},{"key":"3_CR17","unstructured":"Divas\u00f3n, J., Aransay, J.: Hermite normal form. Archive of Formal Proofs, July 2015"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, A.J., P\u00e9rez, M., Varona, J.L.: The Misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them? Not. AMS 61(10), 1249\u20131252 (2014)","DOI":"10.1090\/noti1173"},{"key":"3_CR19","unstructured":"Gamboa, R., Cowles, J., Baalen, J.V.: Using ACL2 arrays to formalise matrix algebra. In: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (2003)"},{"issue":"11","key":"3_CR20","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof - the four-color theorem. Not. AMS 55(11), 1382\u20131393 (2008)","journal-title":"Not. AMS"},{"issue":"4","key":"3_CR21","doi-asserted-by":"publisher","first-page":"837","DOI":"10.1090\/S0894-0347-1989-1002631-0","volume":"2","author":"JL Hafner","year":"1989","unstructured":"Hafner, J.L., McCurley, K.S.: A rigorous subexponential algorithm for computation of class groups. J. Am. Math. Soc. 2(4), 837\u2013850 (1989)","journal-title":"J. Am. Math. Soc."},{"issue":"2","key":"3_CR22","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL Light theory of euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reason."},{"key":"3_CR23","unstructured":"The Haskell Programming Language (2016). \nhttp:\/\/www.haskell.org\/"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Cham (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-319-03545-1_9"},{"key":"3_CR25","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/0024-3795(90)90228-5","volume":"140","author":"MS Hung","year":"1990","unstructured":"Hung, M.S., Rom, W.O.: An application of the Hermite normal form in integer programming. Linear Algebra Appl. 140, 163\u2013179 (1990)","journal-title":"Linear Algebra Appl."},{"issue":"4","key":"3_CR26","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1137\/0608057","volume":"8","author":"E Kaltofen","year":"1987","unstructured":"Kaltofen, E., Krishnamoorthy, M.S., Saunders, B.D.: Fast parallel computation of Hermite and Smith forms of polynomial matrices. SIAM J. Algebraic Discrete Methods 8(4), 683\u2013690 (1987)","journal-title":"SIAM J. Algebraic Discrete Methods"},{"issue":"4","key":"3_CR27","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1137\/0208040","volume":"8","author":"R Kannan","year":"1979","unstructured":"Kannan, R., Bachem, A.: Polynomial algorithms for computing the Smith and Hermite normal forms of an integer matrix. SIAM J. Comput. 8(4), 499\u2013507 (1979)","journal-title":"SIAM J. Comput."},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Klein , G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, SOSP 2009, Big Sky, Montana, USA, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"3_CR29","series-title":"pp","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-319-43144-4_13","volume-title":"Interactive Theorem Proving","author":"O Kun\u010dar","year":"2016","unstructured":"Kun\u010dar, O., Popescu, A.: From types to sets by local type definitions in higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving. pp, pp. 200\u2013218. Springer International Publishing, Cham (2016)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-319-66107-0_23","volume-title":"Interactive Theorem Proving","author":"L Lamb\u00e1n","year":"2017","unstructured":"Lamb\u00e1n, L., Mart\u00edn-Mateos, F.J., Rubio, J., Ruiz-Reina, J.-L.: Using abstract stobjs in ACL2 to compute matrix normal forms. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 354\u2013370. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66107-0_23"},{"key":"3_CR31","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0168-0072(93)90097-W","volume":"59","author":"L Li","year":"1993","unstructured":"Li, L., Li, H., Liu, Y.: A decision algorithm for linear sentences on a PFM. Ann. Pure Appl. Logic 59, 273\u2013286 (1993)","journal-title":"Ann. Pure Appl. Logic"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, 20\u201322 January 2016, pp. 66\u201375 (2016)","DOI":"10.1145\/2854065.2854074"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-11957-6_23","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2010","unstructured":"Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427\u2013447. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-11957-6_23"},{"issue":"4","key":"3_CR34","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10817-015-9320-x","volume":"54","author":"A Narkawicz","year":"2015","unstructured":"Narkawicz, A., Muoz, C., Dutle, A.: Formally-verified decision procedures for univariate polynomial computation based on Sturm\u2019s and Tarski\u2019s theorems. J. Autom. Reason. 54(4), 285\u2013326 (2015)","journal-title":"J. Autom. Reason."},{"key":"3_CR35","volume-title":"Integral Matrices. Pure and Applied Mathematics","author":"M Newman","year":"1972","unstructured":"Newman, M.: Integral Matrices. Pure and Applied Mathematics. Elsevier Science, New York (1972)"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"3_CR37","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic (2018). Updated version of the book with the same title and authors"},{"issue":"3\u20134","key":"3_CR38","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10472-009-9168-z","volume":"56","author":"S Obua","year":"2009","unstructured":"Obua, S., Nipkow, T.: Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell. 56(3\u20134), 245\u2013272 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"3_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9322-8","volume":"55","author":"LC Paulson","year":"2015","unstructured":"Paulson, L.C.: A mechanised proof of G\u00f6del\u2019s incompleteness theorems using nominal Isabelle. J. Autom. Reason. 55(1), 1\u201337 (2015)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"3_CR40","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/BF01206273","volume":"9","author":"J Ramanujam","year":"1995","unstructured":"Ramanujam, J.: Beyond unimodular transformations. J. Supercomput. 9(4), 365\u2013389 (1995)","journal-title":"J. Supercomput."},{"issue":"1\/2","key":"3_CR41","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P Rudnicki","year":"2001","unstructured":"Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative algebra in the Mizar system. J. Symbolic Comput. 32(1\/2), 143\u2013169 (2001)","journal-title":"J. Symbolic Comput."},{"key":"3_CR42","unstructured":"Sternagel, C., Thiemann, R.: Executable matrix operations on matrices of arbitrary dimensions. Archive of Formal Proofs, June 2010"},{"key":"3_CR43","unstructured":"Storjohann, A.: Algorithms for matrix canonical forms. Ph.D. thesis, Swiss Federal Institute of Technology, Zurich (2000)"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle\/HOL. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, 20\u201322 January 2016, pp. 88\u201399 (2016)","DOI":"10.1145\/2854065.2854073"},{"key":"3_CR45","unstructured":"Tourloupis, V.E.: Hermite normal forms and its cryptographic applications. Master\u2019s thesis, University of Wollongong (2013)"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99957-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T04:27:19Z","timestamp":1534825639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99957-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999562","9783319999579"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99957-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}