Integration of multiple formal matrix models in Coq

DOI10.1007/978-3-031-21213-0_11zbMath1528.68396OpenAlexW4312703136MaRDI QIDQ6168985

No author found.

Publication date: 10 August 2023

Published in: Dependable Software Engineering. Theories, Tools, and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-21213-0_11

zbMATH Keywords

Coq theorem proverisomorphic mappingformal matrix theoryinterface and implementation

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Unnamed Item
• Unnamed Item
• A constructive algebraic hierarchy in Coq.
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• First-Class Type Classes
• Canonical Structures for the Working Coq User

This page was built for publication: Integration of multiple formal matrix models in Coq