Title:  Algebraic Formalisation with locales, types and relations
Speakers: Richard Schmoetten
Abstract:

Different approaches have been explored when formalising mathematical structures in Isabelle/HOL, roughly split between the set-based approach using locales and type-based classes. We present our formal theories in Lie groups and real algebra to introduce both ideas, and examine a relation-based way of reasoning about algebraic morphisms in a type class. This has the advantage of integrating directly with automated tooling in Isabelle (the transfer package), and may present an alternative to the current trend of recasting type-based theories as set-based ones (e.g. the Types-to-Sets package).