Generating certified code from formal proofs: a case study in homological algebra
DOI10.1007/S00165-009-0120-0zbMATH Open1214.68330OpenAlexW2102502651WikidataQ57721922 ScholiaQ57721922MaRDI QIDQ968307FDOQ968307
Jesús Aransay, Julio Rubio, Clemens Ballarin
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
Chain complexes (category-theoretic aspects), dg categories (18G35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- 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 (5)
- A Certified Reduction Strategy for Homological Image Processing
- Formalization of a normalization theorem in simplicial topology
- Effective homology of bicomplexes, formalized in Coq
- Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
- Modelling algebraic structures and morphisms in ACL2
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)
