Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

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.

Mon 14 Jan
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at Sala XII
Chair(s): Georges GonthierInria
CPP-201916:00 - 16:30
Research paper
Robert Y. LewisVrije Universiteit Amsterdam
CPP-201916:30 - 17:00
Research paper
Wenda LiUniversity of Cambridge, Lawrence PaulsonUniversity of Cambridge
CPP-201917:00 - 17:30
Research paper