{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,12]],"date-time":"2023-08-12T06:10:24Z","timestamp":1691820624464},"reference-count":31,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T00:00:00Z","timestamp":1436745600000},"content-version":"unspecified","delay-in-days":193,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we present a formalisation in a proof assistant, Isabelle\/HOL, of a<jats:italic>naive<\/jats:italic>version of the Gauss-Jordan algorithm, with explicit proofs of some of its applications; and, additionally, a process to obtain versions of this algorithm in two different functional languages (SML and Haskell) by means of code generation techniques from the verified algorithm. The aim of this research is not to compete with specialised numerical implementations of Gauss-like algorithms, but to show that formal proofs in this area can be used to generate usable functional programs. The obtained programs show compelling performance in comparison to some other verified and functional versions, and accomplish some challenging tasks, such as the computation of determinants of matrices of<jats:italic>big<\/jats:italic>integers and the computation of the homology of matrices representing digital images.<\/jats:p>","DOI":"10.1017\/s0956796815000155","type":"journal-article","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T06:07:32Z","timestamp":1436767652000},"source":"Crossref","is-referenced-by-count":4,"title":["Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm"],"prefix":"10.1017","volume":"25","author":[{"given":"JES\u00daS","family":"ARANSAY","sequence":"first","affiliation":[]},{"given":"JOSE","family":"DIVAS\u00d3N","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,7,13]]},"reference":[{"key":"S0956796815000155_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9260-7"},{"key":"S0956796815000155_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"S0956796815000155_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-72831-5"},{"key":"S0956796815000155_ref27","first-page":"361","volume-title":"Logic and Computer Science","author":"Paulson","year":"1990"},{"key":"S0956796815000155_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2591012"},{"key":"S0956796815000155_ref14","unstructured":"Haftmann F. (2013) Code generation from Isabelle\/HOL theories. Available at: http:\/\/isabelle.in.tum.de\/dist\/Isabelle2013-2\/doc\/codegen.pdf."},{"key":"S0956796815000155_ref13","doi-asserted-by":"crossref","DOI":"10.1201\/b18294","volume-title":"Finite-Dimensional Linear Algebra","author":"Gockenbach","year":"2010"},{"key":"S0956796815000155_ref16","unstructured":"Haftmann F. & Nipkow T. (2010) Code generation via higher-order rewrite systems. In Functional and Logic Programming: 10th International Symposium: FLOPS 2010, Blume M. , Kobayashi N. & Vidal G. (eds), LNCS, vol. 6009. Sendai, Japan: Springer, pp. 103\u2013117."},{"key":"S0956796815000155_ref12","unstructured":"Esparza J. , Lammich P. , Neumann R. , Nipkow T. , Schimpf A. & Smaus J. G. (2013) A fully verified executable LTL model checker, Computer Aided Verification: CAV 2013, Sharygina N. & Veith H. (eds), LNCS, vol. 8044. Saint Petersburg, Russia: Springer, pp. 463\u2013478."},{"key":"S0956796815000155_ref2","unstructured":"Aransay J. & Divas\u00f3n J. (2014b) Gauss-Jordan algorithm and its applications. Arch. Formal Proofs. Available at: http:\/\/afp.sf.net\/entries\/Gauss_Jordan.shtml, Formal proof development."},{"key":"S0956796815000155_ref3","unstructured":"Aransay J. & Divas\u00f3n J. (2014c) Gauss-Jordan elimination in Isabelle\/HOL. Available at: http:\/\/www.unirioja.es\/cu\/jodivaso\/Isabelle\/Gauss-Jordan-2013-2-Generalized\/"},{"key":"S0956796815000155_ref4","unstructured":"Aransay J. & Divas\u00f3n J. (2015) Generalizing a Mathematical Analysis Library in Isabelle\/HOL. NASA Formal Methods, Havelund K. , Holzmann G. & Joshi R. (eds), LNCS, vol. 9058. Pasadena, CA, USA: Springer, pp. 415\u2013421."},{"key":"S0956796815000155_ref6","unstructured":"Avigad J. , H\u00f6lzl J. & Serafin L. (2014) A Formally Verified Proof of the Central Limit Theorem. Available at: http:\/\/arxiv.org\/abs\/1405.7012v1."},{"key":"S0956796815000155_ref7","doi-asserted-by":"crossref","unstructured":"Bulwahn L. , Krauss A. , Haftmann F. , Erk\u00f6k L. & Matthews J. (2008) Imperative functional programming with Isabelle\/HOL. In TPHOLs '08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, O. Mohamed , C. Mu\u00f1oz & Tahar S. (eds), LNCS, vol. 5170. Montreal, Canada: Springer, pp. 352\u2013367.","DOI":"10.1007\/978-3-540-71067-7_14"},{"key":"S0956796815000155_ref8","unstructured":"D\u00e9n\u00e8s M. (2013) \u00c9tude Formelle d'algorithmes Efficaces En Alg\u00e8bre Lin\u00e9aire. PhD Thesis, INRIA Sophia Antipolis, France."},{"key":"S0956796815000155_ref9","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 ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Beringer L. & Felty A. (eds), LNCS, vol. 7406. Princeton, NJ, USA: Springer, pp. 83\u201398.","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"S0956796815000155_ref10","first-page":"147","volume-title":"Certified Programs and Proofs","author":"D\u00e9n\u00e8s","year":"2013"},{"key":"S0956796815000155_ref11","doi-asserted-by":"publisher","DOI":"10.1090\/noti1173"},{"key":"S0956796815000155_ref15","doi-asserted-by":"crossref","unstructured":"Haftmann F. , Krauss A. , Kuncar O. & Nipkow T. (2013) Data refinement in Isabelle\/HOL. In Interactive Theorem Proving: ITP 2013, Blazy S. , Paulin-Mohring C. , & Pichardie D. (eds), LNCS, vol. 7998. Rennes, France: Springer, pp. 100\u2013115.","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"S0956796815000155_ref17","volume-title":"The Kepler Conjecture. The Hales-Ferguson Proof","author":"Hales","year":"2011"},{"key":"S0956796815000155_ref18","doi-asserted-by":"crossref","unstructured":"Harrison J. (2005) A HOL theory of Euclidean space. In Theorem Proving in Higher Order Logics, Hurd J. & Melham T. (eds), LNCS, vol. 3603. Oxford, UK: Springer, pp. 114\u2013129.","DOI":"10.1007\/11541868_8"},{"key":"S0956796815000155_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9250-9"},{"key":"S0956796815000155_ref20","unstructured":"Haskell. (2014) The Haskell Programming Language. Available at: http:\/\/www.haskell.org\/."},{"key":"S0956796815000155_ref21","doi-asserted-by":"crossref","unstructured":"Heras J. , D\u00e9n\u00e8s M. , Mata G. , M\u00f6rtberg A. , Poza M. & Siles V. (2012) Towards a certified computation of homology groups for digital images. In Computational Topology in Image Context: CTIC 2012, Ferri M. , Frosini P. , Landi C. , Cerri A. & Fabio B. D. (eds), LNCS, vol. 7309. Bertinoro, Italy: Springer, pp. 49\u201357.","DOI":"10.1007\/978-3-642-30238-1_6"},{"key":"S0956796815000155_ref22","unstructured":"HMA. (2014) HOL Multivariate Analysis Library. Available at: http:\/\/isabelle.in.tum.de\/library\/HOL\/HOL-Multivariate_Analysis\/index.html."},{"key":"S0956796815000155_ref24","unstructured":"MLton. (2014) The MLton website. Available at: http:\/\/mlton.org\/."},{"key":"S0956796815000155_ref28","unstructured":"Poly M. L. (2014) The Poly\/ML website. Available at: http:\/\/www.polyml.org\/."},{"key":"S0956796815000155_ref31","volume-title":"Introduction to Linear Algebra","author":"Strang","year":"2009"},{"key":"S0956796815000155_ref1","doi-asserted-by":"crossref","unstructured":"Aransay J. & Divas\u00f3n J. (2014a) Formalization and execution of Linear Algebra: From theorems to algorithms. In Post Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation: LOPSTR 2013, Gupta G. & Pe\u00f1a R. (eds), LNCS, vol. 8901. Madrid, Spain: Springer, pp. 01\u201319.","DOI":"10.1007\/978-3-319-14125-1_1"},{"key":"S0956796815000155_ref23","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML, revised edition","author":"Milner","year":"1997"},{"key":"S0956796815000155_ref25","unstructured":"Nipkow T. (2011) Gauss-Jordan elimination for matrices represented as functions. Arch. Formal Proofs. Available at: http:\/\/afp.sf.net\/entries\/Gauss-Jordan-Elim-Fun.shtml, Formal proof development."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796815000155","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,12]],"date-time":"2023-08-12T05:29:51Z","timestamp":1691818191000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796815000155\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":31,"alternative-id":["S0956796815000155"],"URL":"https:\/\/doi.org\/10.1017\/s0956796815000155","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"article-number":"e9"}}