![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Thursday 16 March 2023, 17:00-18:00
The Locale-Centric Approach for Formalising Mathematical Hierarchies
- đ¤ Speaker: Chelsea Edmonds (University of Cambridge) đ Website
- đ Date & Time: Thursday 16 March 2023, 17:00 - 18:00
- đ Venue: Centre for Mathematical Sciences MR12, CMS
Abstract
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.
Series This talk is part of the Formalisation of mathematics with interactive theorem provers series.
Included in Lists
- All CMS events
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Centre for Mathematical Sciences MR12, CMS
- CMS Events
- Department of Computer Science and Technology talks and seminars
- DPMMS info aggregator
- DPMMS lists
- DPMMS Lists
- DPMMS Pure Maths study groups
- Formalisation of mathematics with interactive theorem provers
- Hanchen DaDaDash
- Interested Talks
- Martin's interesting talks
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- yk449
Note: Ex-directory lists are not shown.