Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm

  1. Aransay, J. 1
  2. Divasón, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
Journal of Functional Programming

ISSN: 0956-7968

Año de publicación: 2015

Volumen: 25

Número: 1

Páginas: 1-21

Tipo: Artículo

DOI: 10.1017/S0956796815000155 SCOPUS: 2-s2.0-84993960775 WoS: WOS:000368240300002 GOOGLE SCHOLAR lock_openAcceso abierto editor

Otras publicaciones en: Journal of Functional Programming

Repositorio institucional: lockAcceso abierto Editor

Resumen

In this paper, we present a formalisation in a proof assistant, Isabelle/HOL, of a naive 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 big integers and the computation of the homology of matrices representing digital images