TITLE: Formalisation of a theory of packages in Coq
SPEAKER: Jaap Boender (Middlesex University)

ABSTRACT:

Over the years, open source distributions have become increasingly large and complex---as an example, the latest Debian distribution contains almost 30 000 packages.

Consequently, the tools that deal with these distribution have also become more and more complex. Furthermore, to deal with increasing distribution sizes optimisation has become more important as well.

To make sure that correctness is not sacrificed for complexity and optimisation, it is important to verify the underlying assumptions formally.

This presentation will involve the formalisation and verification of the 'theory of packages' - a mathematical model of a packaging system - using Coq, as a gentle introduction to how Coq works and how it can be used.