Generating certified code from formal proofs: a case study in homological algebra
From MaRDI portal
Publication:968307
DOI10.1007/s00165-009-0120-0zbMath1214.68330OpenAlexW2102502651WikidataQ57721922 ScholiaQ57721922MaRDI QIDQ968307
Jesús Aransay, Clemens Ballarin, Julio Jesús Rubio García
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Formalization of a normalization theorem in simplicial topology ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ 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
Cites Work
- Unnamed Item
- Unnamed Item
- A mechanized proof of the basic perturbation lemma
- Adapting functional programs to higher order logic
- An object-oriented interpretation of the EAT system
- Isabelle/HOL. A proof assistant for higher-order logic
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Flyspeck II: The basic linear programs
- On the chain-complex of a fibration
- A Modular Formalisation of Finite Group Theory
- Proof Pearl: Looping Around the Orbit
- A Fixed Point Approach to Homological Perturbation Theory
- Computer Aided Systems Theory – EUROCAST 2005
- Towards Constructive Homological Algebra in Type Theory
- Object oriented institutions to specify symbolic computation systems
- Artificial Intelligence and Symbolic Computation
- Theorem Proving in Higher Order Logics
- Types for Proofs and Programs
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
This page was built for publication: Generating certified code from formal proofs: a case study in homological algebra
