Integration of multiple formal matrix models in Coq

DOI10.1007/978-3-031-21213-0_11MaRDI QIDQ6168985zbMATH OpenOpenAlexFDO

Authors

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 proverformal matrix theoryinterface and implementationisomorphic mapping

Mathematics Subject Classification ID

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

Recommendations

• Formalization of operations of block matrix based on Coq
• Incidence simplicial matrices formalized in Coq/SSReflect
• Formalizing implicative algebras in Coq
• Formalizing generalized maps in Coq
• Coherent models of proof nets
• Formalized, effective domain theory in Coq
• Toward a formal theory of model integration
• A Coq formalization of finitely presented modules
• Modular Development of Hybrid Systems for Verification in Coq

Cites work

• A constructive algebraic hierarchy in Coq.
• Canonical structures for the working Coq user
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• First-Class Type Classes
• Formalization of operations of block matrix based on Coq
• Overview of formal methods

Cited in

(1)

• Formalizing the Cholesky factorization theorem

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6168985)