Generating certified code from Formal Proofs: a case study in Homological Algebra

  1. Aransay, J. 1
  2. Ballarin, C. 2
  3. Rubio, J. 1
  1. 1 Universidad de La Rioja

    Universidad de La Rioja

    Logroño, España

    GRID grid.119021.a

  2. 2 Technical University Munich

    Technical University Munich

    Múnich, Alemania

    GRID grid.6936.a

Formal Aspects of Computing

ISSN: 0934-5043

Year of publication: 2010

Volume: 22

Issue: 2

Pages: 193-213

Type: Article

Export: RIS
DOI: 10.1007/s00165-009-0120-0 SCOPUS: 2-s2.0-77954039566 WoS: 000275414900005 lock_openOpen access editor
bar_chart See metrics


We apply current theoremproving technology to certified code in the domain of abstract algebra. More concretely, based on a formal proof of the Basic Perturbation Lemma (a central result in homological algebra) in the prover Isabelle/HOL, we apply various code generation techniques, which lead to certified implementations of the associated algorithm inML. In the formal proof, algebraic structures occurring in the Basic Perturbation Lemma are represented in a way, which is not directly amenable to code generation with the available tools. Interestingly, this representation is required in the proof, while for the algorithm simpler data structures are sufficient. Our approach is to establish a link between the non-executable setting of the proof and the executable representation in the algorithm, which is to be generated. This correspondence is established within the logical framework of Isabelle/HOL-that is, it is formally proved correct. The generated code is applied to and illustrated with a number of examples. BCS © 2009.