Title: Manifold Theory in Isabelle/HOL
Speakers: Richard Schmoetten
Abstract:

I will give a whirlwind tour of my work in the formalisation of manifolds in Isabelle/HOL, and I will show how to get around the restrictions of simple types to formalise interesting properties of vector fields. To motivate doing all this theory, I will preface my talk with a selection of example applications of manifolds.