Effective homology of bicomplexes, formalized in Coq
type: Item
instance of: scholarly article
title: Effective homology of bicomplexes, formalized in Coq
zbMATH Open document ID: 1207.68211
author: César Domínguez
author: Julio Rubio
published in: Theoretical Computer Science
publication date: 2011-03-14T00:00:00Z
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 55U15
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68W30
zbMATH DE Number: 5865584
zbMATH Keywords: theorem proving
zbMATH Keywords: formal methods
zbMATH Keywords: computer algebra
zbMATH Keywords: program verification
zbMATH Keywords: Coq theorem prover
zbMATH Keywords: Coq proof assistant
describes a project that uses: EAT
describes a project that uses: Flyspeck
describes a project that uses: Kenzo
describes a project that uses: Coq
MaRDI profile type: Publication
full work available at URL: j.tcs.2010.11.016
OpenAlex ID: W2036798279
cites work: A mechanized proof of the basic perturbation lemma
cites work: Generating certified code from formal proofs: a case study in homological algebra
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: On the correctness of upper layers of automotive systems
cites work: Calculemus
cites work: Q3062067
cites work: Towards Constructive Homological Algebra in Type Theory
cites work: Diagrammatic logic applied to a parameterisation process
cites work: Object oriented institutions to specify symbolic computation systems
cites work: Q3655278
cites work: Q4693118
cites work: A constructive algebraic hierarchy in Coq.
cites work: Q5302559
cites work: A Modular Formalisation of Finite Group Theory
cites work: An object-oriented interpretation of the EAT system
cites work: Flyspeck II: The basic linear programs
cites work: Q3787156
cites work: Constructive algebraic topology
cites work: The computability problem in algebraic topology
cites work: Developing the Algebraic Hierarchy with Type Classes in Coq
DOI: 10.1016/J.TCS.2010.11.016
description: scientific article; zbMATH DE number 5865584