Incidence Simplicial Matrices Formalized in Coq/SSReflect
From MaRDI portal
Publication:5200106
DOI10.1007/978-3-642-22673-1_3zbMath1335.68229OpenAlexW164581696MaRDI QIDQ5200106
Laurence Rideau, Maxime Dénès, Jónathan Heras, María Poza
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00603208/file/ismfis.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Incidence Simplicial Matrices Formalized in Coq/SSReflect
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Effective homology of bicomplexes, formalized in Coq
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Spinor groups and algebraic coding theory
- A mechanized proof of the basic perturbation lemma
- Asymptotically efficient triangulations of the \(d\)-cube
- On the cohomology of 3D digital images
- Homotopy in digital spaces
- A Modular Formalisation of Finite Group Theory
- Canonical Big Operators
- Incidence Simplicial Matrices Formalized in Coq/SSReflect
- Computer Algebra in Scientific Computing
This page was built for publication: Incidence Simplicial Matrices Formalized in Coq/SSReflect
