{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:03:12Z","timestamp":1762459392782},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T00:00:00Z","timestamp":1477958400000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this contribution we present a formalised algorithm in the Isabelle\/HOL proof assistant to compute echelon forms, and, as a consequence, characteristic polynomials of matrices. We have proved its correctness over B\u00e9zout domains, but its executability is only guaranteed over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This is possible since the algorithm has been parameterised by a (possibly non-computable) operation that returns the B\u00e9zout coefficients of a pair of elements of a ring. The echelon form is also used to compute determinants and inverses of matrices. As a by-product, some algebraic structures have been implemented (principal ideal domains, B\u00e9zout domains, etc.). In order to improve performance, the algorithm has been refined to immutable arrays inside of Isabelle and code can be generated to functional languages as well.<\/jats:p>","DOI":"10.1007\/s00165-016-0383-1","type":"journal-article","created":{"date-parts":[[2016,6,28]],"date-time":"2016-06-28T07:20:25Z","timestamp":1467098425000},"page":"1005-1026","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formalisation of the computation of the echelon form of a matrix in Isabelle\/HOL"],"prefix":"10.1145","volume":"28","author":[{"given":"Jes\u00fas","family":"Aransay","sequence":"first","affiliation":[{"name":"Departamento de Matem\u00e1ticas y Computaci\u00f3n, C\/ Luis de Ulloa 2, Edificio Juan Luis Vives, Universidad de La Rioja, 26004, Logro\u00f1o, La Rioja, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose","family":"Divas\u00f3n","sequence":"additional","affiliation":[{"name":"Departamento de Matem\u00e1ticas y Computaci\u00f3n, C\/ Luis de Ulloa 2, Edificio Juan Luis Vives, Universidad de La Rioja, 26004, Logro\u00f1o, La Rioja, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"#cr-split#-e_1_2_1_2_1_2.1","doi-asserted-by":"crossref","unstructured":"Aransay J Divas\u00f3n J (2014) Formalization and execution of Linear Algebra: from theorems to algorithms. In: Gupta G Pe\u00f1a R","DOI":"10.1007\/978-3-319-14125-1_1"},{"key":"#cr-split#-e_1_2_1_2_1_2.2","unstructured":"(ed) Post Proceedings of the international symposium on logic-based program synthesis and transformation: LOPSTR 2013 LNCS vol 8901. Springer pp 01-19"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Aransay J Divas\u00f3n J (2015) Formalisation in higher-order logic and code generation to functional languages of the Gauss\u2013Jordan algorithm. J Funct Program 25(e9):21. doi:10.1017\/S0956796815000155","DOI":"10.1017\/S0956796815000155"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aransay J Divas\u00f3n J (2015) Generalizing a Mathematical Analysis library in Isabelle\/HOL. In: Havelund K Holzmann G Joshi R (eds) Proceedings of the seventh NASA formal methods symposium: NFM 2015","DOI":"10.1007\/978-3-319-17524-9_30"},{"key":"e_1_2_1_2_4_2","unstructured":"Adelsberger S Hetzl S Pollak F (2014) The Cayley\u2013Hamilton theorem. Archive of formal proofs. Formal proof development. http:\/\/isa-afp.org\/entries\/Cayley_Hamilton.shtml. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_5_2","volume-title":"Computational fluid and solid mechanics","author":"Bathe KJ","year":"2003"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)90766-5"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Beineke LW Wilson RJ (2004) Topics in algebraic graph theory. Encyclopedia of mathematics and its applications. Cambridge University Press Cambridge","DOI":"10.1017\/CBO9780511529993"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Cano G Cohen C D\u00e9n\u00e8s M M\u00f6rtberg A Siles V (2016) Formalized linear algebra over elementary divisor rings in Coq. Logical methods in computer science (Submitted)","DOI":"10.2168\/LMCS-12(2:7)2016"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cohen C D\u00e9n\u00e8s M M\u00f6rtberg A (2013) Refinements for Free! In: Gonthier G Norrish M (eds) Certified programs and proofs: CPP 2013 of lecture notes in computer science vol 8307. Springer pp 147\u2013162","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_2_1_2_10_2","volume-title":"The essentials of factor analysis","author":"Child D","year":"2006"},{"key":"e_1_2_1_2_11_2","unstructured":"Divas\u00f3n J Aransay J (2014) Gauss\u2013Jordan algorithm and Its applications. Archive of formal proofs. Formal proof development. http:\/\/isa-afp.org\/entries\/Gauss_Jordan.shtml. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_12_2","unstructured":"Divas\u00f3n J Aransay J (2015) Echelon form. Archive of formal proofs. http:\/\/isa-afp.org\/entries\/Echelon_Form.shtml Formal proof development. Updated version available from the AFP repository version: http:\/\/www.isa-afp.org\/devel-entries\/Echelon_Form.shtml. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_13_2","unstructured":"Divas\u00f3n J Aransay J (2015) QR Decomposition. Archive of formal proofs. Formal proof development. http:\/\/isa-afp.org\/entries\/QR_Decomposition.shtml. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_14_2","unstructured":"D\u00e9n\u00e8s M (2013) Formal study of efficient algorithms in linear algebra. Ph.D. thesis Universit\u00e9 Nice Sophia Antipolis"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"D\u00e9n\u00e8s M M\u00f6rtberg A Siles V (2012) A refinement-based approach to Computational Algebra in COQ. In: Beringer L Felty A (eds) Interactive theorem proving: ITP 2012 lecture notes in computer science vol 7406. Springer pp 83\u201398","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Eberl M (2015) A decision procedure for univariate real polynomials in Isabelle\/HOL. In: Proceedings of the 2015 conference on certified programs and proofs CPP \u201915 New York NY USA pp 75\u201383","DOI":"10.1145\/2676724.2693166"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Fuchs L Salce L (2001) Modules over non-Noetherian domains. Mathematical surveys and monographs. American Mathematical Society Providence","DOI":"10.1090\/surv\/084"},{"key":"e_1_2_1_2_18_2","unstructured":"Fukunaga K (2013) Introduction to statistical pattern recognition. Computer science and scientific computing. Elsevier Science Amsterdam"},{"key":"e_1_2_1_2_19_2","unstructured":"Gamboa R Cowles J Van Baalen J (2003) Using ACL2 arrays to formalise matrix algebra. In: Fourth international workshop on the ACL2 theorem prover and its applications"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hales T Adams M Bauer G Tat Dang D Harrison J Le Hoang T Kaliszyk C Magron V McLaughlin S Tat Nguyen T Quang Nguyen T Nipkow T Obua S Pleso J Rute J Solovyev A Hoai Thi Ta A Tran TN Thi Trieu D Urban J Khac Vu K Zumkeller R (2015) Formal proof of the Kepler conjecture CoRR. abs\/1501.02155. Accessed 30 Apr 2016","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_2_1_2_21_2","unstructured":"Haftmann F (2016) Code generation from Isabelle\/HOL theories. Tutorial documentation. http:\/\/isabelle.in.tum.de\/dist\/Isabelle2016\/doc\/codegen.pdf. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_22_2","unstructured":"Haftmann F (2016) Haskell-style type classes with Isabelle\/Isar. Tutorial documentation. http:\/\/isabelle.in.tum.de\/dist\/Isabelle2016\/doc\/classes.pdf. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9250-9"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Huffman B Kun\u010dar O (2013) Lifting and Transfer: A Modular Design for Quotients in Isabelle\/HOL. In: Gonthier G Norrish M (eds) Certified programs and proofs: CPP 2013 lecture notes in computer science vol 8307. Springer pp 131\u2013146","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_2_1_2_25_2","volume-title":"Handbook of linear algebra (discrete mathematics and its applications), 1st edn","author":"Hogben J","year":"2006"},{"key":"e_1_2_1_2_26_2","unstructured":"Jacobson N (2012) Basic algebra I 2nd edn. Dover Books on Mathematics Dover Publications New York"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Klein G Elphinstone K Heiser G Andronick J Cock D Derrin P Elkaduwe D Engelhardt K Kolanski R Norrish M Sewell T Tuch H Winwood S (2009) seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22Nd symposium on operating systems principles SOSP \u201909. ACM New York pp 207\u2013220","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Lochbihler A Bulwahn L (2011) Animating the formalised semantics of a Java-like Language. In: van Eekelen M Geuvers H Schmalz J Wiedijk F (eds) Interactive theorem proving (ITP 2011) lecture notes in computer science vol 6898. Springer pp 216 \u2013 232","DOI":"10.1007\/978-3-642-22863-6_17"},{"key":"e_1_2_1_2_29_2","unstructured":"Leon SJ (2014) Linear algebra with applications. Featured titles for linear algebra (introductory) Series. Pearson Education New Jersey"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Liu B Lai HJ (2000) Matrices in combinatorics and graph theory. Network theory and applications. Springer Berlin","DOI":"10.1007\/978-1-4757-3165-1"},{"key":"e_1_2_1_2_31_2","unstructured":"Langville AN Meyer CD (2011) Google\u2019s Pagerank and beyond: the science of search engine rankings. Princeton University Press Princeton"},{"key":"e_1_2_1_2_32_2","unstructured":"The MLton website. MLton. a whole program optimizing complier for Standard ML. http:\/\/mlton.org\/. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_33_2","unstructured":"Newman M (1972) Integral matrices. Pure and applied mathematics. Elsevier Science New York"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9320-x"},{"key":"e_1_2_1_2_35_2","unstructured":"Ould Biha S (2010) Mathematical components for groups theory. Ph.D. thesis Universit\u00e9 Nice Sophia Antipolis"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3032"},{"key":"e_1_2_1_2_37_2","unstructured":"The Poly\/ML website. http:\/\/www.polyml.org\/. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Roman S (2007) Advanced linear algebra. Graduate texts in mathematics. Springer Berlin","DOI":"10.1007\/978-0-387-72831-5"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0456"},{"key":"e_1_2_1_2_40_2","unstructured":"Storjohann A (2000) Algorithms for matrix canonical forms. Ph.D. thesis Swiss Federal Institute of Technology Zurich"},{"issue":"1","key":"e_1_2_1_2_41_2","first-page":"27","article-title":"A formal proof of Sasaki\u2013Murao algorithm","volume":"5","author":"Coquand T","year":"2012","journal-title":"J Formaliz Reason"},{"key":"e_1_2_1_2_42_2","unstructured":"Thiemann R Yamada A (2015) Matrices Jordan normal forms and spectral radius theory. Archive of formal proofs August. Formal proof development. http:\/\/isa-afp.org\/entries\/Jordan_Normal_Form.shtml. Accessed 30 Apr 2016"},{"key":"e_1_2_1_2_43_2","unstructured":"Von Neumann J (1955) Mathematical foundations of quantum mechanics. Investigations in physics. Princeton University Press Princeton"},{"key":"e_1_2_1_2_44_2","volume-title":"A first course in differential equations with modeling applications","author":"Zill D","year":"2012"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0383-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0383-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0383-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0383-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:05:48Z","timestamp":1641485148000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0383-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":45,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2016,11]]}},"alternative-id":["10.1007\/s00165-016-0383-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0383-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11]]}}}