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

Displayed time zone: Belfast change

16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Georges Gonthier Inria
16:00
30m
Research paper
A Formal Proof of Hensel's Lemma over the p-adic Integers
CPP
Robert Y. Lewis Vrije Universiteit Amsterdam
DOI
16:30
30m
Research paper
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
CPP
Wenda Li University of Cambridge, Lawrence Paulson University of Cambridge
DOI
17:00
30m
Research paper
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
CPP
DOI