BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A modular approach to formalising combinatorial structures - Chels
 ea Edmonds (University of Cambridge)
DTSTART:20210709T100000Z
DTEND:20210709T110000Z
UID:TALK160792@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:Combinatorial design theory studies set systems with certain b
 alance and symmetry properties. It has applications in many areas of compu
 ter science and engineering\, including safety and security critical syste
 ms\, yet has never previously been formalised in any system.\n\nIn this ta
 lk\, I'll present a modular approach to formalising designs using Isabelle
 /HOL. I'll discuss how locales\, Isabelle's module system\, can be used to
  specify numerous types of designs and manage their complex hierarchy. The
  resultant library has formal definitions and proofs for many key properti
 es\, operations\, and theorems on the construction and existence of design
 s. Additionally\, it has proven to be highly flexible and extensible throu
 gh several different formalisation extensions. To finish\, I'll discuss th
 e applicability of this locale-centric approach to future formalisations o
 f complex mathematical hierarchies in simple type theory.\n\nNo previous k
 nowledge of design theory is required. This is a slightly longer version o
 f a talk for an external conference\, so feedback is very welcome.
LOCATION:https://meet.google.com/jxy-edcv-wgx
END:VEVENT
END:VCALENDAR