The Locale-Centric Approach for Formalising Mathematical Hierarchies

Add to your list(s) Download to your calendar using vCal

• Chelsea Edmonds (University of Cambridge)
• Thursday 16 March 2023, 17:00-18:00
• Centre for Mathematical Sciences MR12, CMS.

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki.

Locales are Isabelle’s module system and have been around for over 20 years. Yet it is only in the last few years that we have fully begun to explore the potential of locales as a basis for formalising a wide varieties of structures, particularly in mathematics. This talk will both provide an introduction to locales and give an overview of recent achievements, with a later focus on my own work in formalising large hierarchies of combinatorial structures such as graphs, hypergraphs, and designs. This will particularly examine the potential locales offer for transfer of information and the modularity, flexibility and extensibility of formal libraries. Additionally, I’ll give some examples of various proof techniques that make working with locales simple. The talk will conclude with a discussion on some of the strengths and weaknesses of locales, including some comparisons to other similar tools in both Isabelle and other proof assistants.

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• Centre for Mathematical Sciences MR12, CMS
• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.