Generating certified code from formal proofs: a case study in homological algebra

DOI10.1007/S00165-009-0120-0MaRDI QIDQ968307zbMATHOpenAlexWikidataFDO

Authors Jesús Aransay, Clemens Ballarin, Julio Rubio

Publication date 5 May 2010

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-009-0120-0

zbMATH Keywords

homological algebraIsabelle/HOLcode generationformalized mathematicssoftware certification

Mathematics Subject Classification ID

Chain complexes (category-theoretic aspects), dg categories (18G35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A mechanized proof of the basic perturbation lemma
• Artificial Intelligence and Symbolic Computation
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• A Coq formalization of finitely presented modules
• Effective homology of bicomplexes, formalized in Coq

Cites work

• scientific article; zbMATH DE number 1301860 (Why is no real title available?)
• scientific article; zbMATH DE number 2003148 (Why is no real title available?)
• A Fixed Point Approach to Homological Perturbation Theory
• A Modular Formalisation of Finite Group Theory
• A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
• A mechanized proof of the basic perturbation lemma
• Adapting functional programs to higher order logic
• An object-oriented interpretation of the EAT system
• Artificial Intelligence and Symbolic Computation
• Computer Aided Systems Theory – EUROCAST 2005
• Flyspeck II: The basic linear programs
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Isabelle/HOL. A proof assistant for higher-order logic
• Object oriented institutions to specify symbolic computation systems
• On the chain-complex of a fibration
• Proof Pearl: Looping Around the Orbit
• Theorem Proving in Higher Order Logics
• Towards Constructive Homological Algebra in Type Theory
• Types for Proofs and Programs

Cited in

(7)

• Formalization of a normalization theorem in simplicial topology
• Effective homology of bicomplexes, formalized in Coq
• A certified reduction strategy for homological image processing
• Artificial Intelligence and Symbolic Computation
• Modelling algebraic structures and morphisms in ACL2
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Proving with ACL2 the correctness of simplicial sets in the Kenzo system

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• Isar
• Kenzo
• EAT
• Flyspeck

This page was built for publication: Generating certified code from formal proofs: a case study in homological algebra

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q968307)