Smooth manifolds and types to sets for linear algebra in Isabelle/HOL.
CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs Cascais Portugal January, 2019(2019)
摘要
We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem for line integrals. We also construct some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the existing libraries for topology and analysis. The existing library for linear algebra is not flexible enough for our needs. We therefore set up the first systematic and large scale application of ``types to sets''. It allows us to automatically transform the existing (type based) library of linear algebra to one with explicit carrier sets.
更多查看译文
关键词
Isabelle, Higher Order Logic, Manifolds, Formalization of Mathematics
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络