Generating certified code from formal proofs: a case study in homological algebra
DOI10.1007/S00165-009-0120-0zbMATH Open1214.68330OpenAlexW2102502651WikidataQ57721922 ScholiaQ57721922MaRDI QIDQ968307FDOQ968307
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
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
Chain complexes (category-theoretic aspects), dg categories (18G35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Towards Constructive Homological Algebra in Type Theory
- Isabelle/HOL. A proof assistant for higher-order logic
- A Modular Formalisation of Finite Group Theory
- Types for Proofs and Programs
- On the chain-complex of a fibration
- A Fixed Point Approach to Homological Perturbation Theory
- An object-oriented interpretation of the EAT system
- Flyspeck II: The basic linear programs
- Object oriented institutions to specify symbolic computation systems
- A mechanized proof of the basic perturbation lemma
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Title not available (Why is that?)
- Adapting functional programs to higher order logic
- Proof Pearl: Looping Around the Orbit
- Computer Aided Systems Theory – EUROCAST 2005
- Artificial Intelligence and Symbolic Computation
Cited In (7)
- A certified reduction strategy for homological image processing
- Proving with ACL2 the correctness of simplicial sets in the Kenzo system
- Formalization of a normalization theorem in simplicial topology
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Effective homology of bicomplexes, formalized in Coq
- Modelling algebraic structures and morphisms in ACL2
- Artificial Intelligence and Symbolic Computation
Uses Software
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)
