Generating certified code from formal proofs: a case study in homological algebra
type: Item
instance of: scholarly article
title: Generating certified code from formal proofs: a case study in homological algebra
zbMATH Open document ID: 1214.68330
author: Jesús Aransay
author: Clemens Ballarin
author: Julio Rubio
published in: Formal Aspects of Computing
publication date: 2010-05-05T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 18G35
Mathematics Subject Classification ID: 68N30
zbMATH DE Number: 5703857
zbMATH Keywords: formalized mathematics
zbMATH Keywords: software certification
zbMATH Keywords: code generation
zbMATH Keywords: homological algebra
zbMATH Keywords: Isabelle/HOL
describes a project that uses: Isabelle
describes a project that uses: EAT
describes a project that uses: Flyspeck
describes a project that uses: Isabelle/HOL
describes a project that uses: Isar
describes a project that uses: Kenzo
MaRDI profile type: Publication
full work available at URL: s00165-009-0120-0
OpenAlex ID: W2102502651
Wikidata QID: Q57721922
cites work: Artificial Intelligence and Symbolic Computation
cites work: Computer Aided Systems Theory – EUROCAST 2005
cites work: A mechanized proof of the basic perturbation lemma
cites work: Types for Proofs and Programs
cites work: Interpretation of Locales in Isabelle: Theories and Proof Contexts
cites work: Q4435458
cites work: A Fixed Point Approach to Homological Perturbation Theory
cites work: Towards Constructive Homological Algebra in Type Theory
cites work: Object oriented institutions to specify symbolic computation systems
cites work: A Modular Formalisation of Finite Group Theory
cites work: On the chain-complex of a fibration
cites work: A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
cites work: An object-oriented interpretation of the EAT system
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q4247084
cites work: Theorem Proving in Higher Order Logics
cites work: Proof Pearl: Looping Around the Orbit
cites work: Flyspeck II: The basic linear programs
cites work: Adapting functional programs to higher order logic
DOI: 10.1007/S00165-009-0120-0
description: scientific article; zbMATH DE number 5703857