BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Locale-Centric Approach for Formalising Mathematical Hierarchi
 es - Chelsea Edmonds (University of Cambridge)
DTSTART:20230316T170000Z
DTEND:20230316T180000Z
UID:TALK193723@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION: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 beg
 un to explore the potential of locales as a basis for formalising a wide v
 arieties of structures\, particularly in mathematics. This talk will both 
 provide an introduction to locales and give an overview of recent achievem
 ents\, with a later focus on my own work in formalising large hierarchies 
 of combinatorial structures such as graphs\, hypergraphs\, and designs. Th
 is will particularly examine the potential locales offer for transfer of i
 nformation and the modularity\, flexibility and extensibility of formal li
 braries. Additionally\, I'll give some examples of various proof technique
 s that make working with locales simple. The talk will conclude with a dis
 cussion on some of the strengths and weaknesses of locales\, including som
 e comparisons to other similar tools in both Isabelle and other proof assi
 stants.\n
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR