A modular approach to formalising combinatorial structures

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

• Chelsea Edmonds (University of Cambridge)
• Friday 09 July 2021, 11:00-12:00
• https://meet.google.com/jxy-edcv-wgx.

If you have a question about this talk, please contact Nathanael Arkor.

Combinatorial design theory studies set systems with certain balance and symmetry properties. It has applications in many areas of computer science and engineering, including safety and security critical systems, yet has never previously been formalised in any system.

In this talk, 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 properties, operations, and theorems on the construction and existence of designs. Additionally, it has proven to be highly flexible and extensible through several different formalisation extensions. To finish, I’ll discuss the applicability of this locale-centric approach to future formalisations of complex mathematical hierarchies in simple type theory.

No previous knowledge of design theory is required. This is a slightly longer version of a talk for an external conference, so feedback is very welcome.

This talk is part of the Logic & Semantics for Dummies series.

This talk is included in these lists:

• Logic & Semantics for Dummies
• https://meet.google.com/jxy-edcv-wgx
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.