BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &\; Semantics for Dummies
SUMMARY:A modular approach to formalising combinatorial st
ructures - Chelsea Edmonds (University of Cambridg
e)
DTSTART;TZID=Europe/London:20210709T110000
DTEND;TZID=Europe/London:20210709T120000
UID:TALK160792AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/160792
DESCRIPTION:Combinatorial design theory studies set systems wi
th certain balance and symmetry properties. It has
applications in many areas of computer science an
d engineering\, including safety and security crit
ical systems\, yet has never previously been forma
lised in any system.\n\nIn this talk\, I'll presen
t 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 hierarch
y. The resultant library has formal definitions an
d proofs for many key properties\, operations\, an
d theorems on the construction and existence of de
signs. Additionally\, it has proven to be highly f
lexible and extensible through several different f
ormalisation extensions. To finish\, I'll discuss
the applicability of this locale-centric approach
to future formalisations of complex mathematical h
ierarchies in simple type theory.\n\nNo previous k
nowledge of design theory is required. This is a s
lightly longer version of a talk for an external c
onference\, so feedback is very welcome.
LOCATION:https://meet.google.com/jxy-edcv-wgx
CONTACT:Nathanael Arkor
END:VEVENT
END:VCALENDAR