Skip to content
Date: 27th June 2023
Time: 10:00 - 11:00
Location: IF 1.16

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

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).