Programming and formal software verification
This talk, presented at the seL4 Summit, October 2022, gives an introduction to the seL4 integrity theorems. The integrity theorems were first published in 2011, and they show how seL4 can enforce access control policies. The talk explains what the theorems mean, and how to apply them to both static and dynamic seL4-based systems. Also on YouTube. MP4 downloads are available from Vimeo. Slides are…
This screencast gives a guided tour of the Isabelle/HOL proofs about the seL4 microkernel, focussing mainly on the abstract specification and some of the properties we prove about it. It was given as a pre-recorded talk for the third seL4 Summit, held virtually in November 2020. The talk assumes some familiarity with seL4, but aims to be accessible to people without previous experience of formal…
Pattern matching with dependent types in Coq can be awkward, while equivalent programs in Agda might be straightforward and elegant. Yet despite the awkwardness, there may still be reasons to choose Coq for your next dependently-typed development, for example if you want a tactic language to develop domain-specific proof-search procedures. In this talk, we show how to match in Coq, using…
This post is an extended version of a lightning talk I gave at the Brisbane Functional Programming Group. It introduces the difference list, a simple trick for improving the performance of certain kinds of list-building functions in Haskell, and goes on to explore the connections to monoids and folds. The first half is aimed at Haskell novices, while the latter parts might be interesting to…
Here’s a little exercise for anyone who, like me, recently came across Scott Meyers’ work on universal references in C++11: Is the following program well formed? Does it have well-defined behaviour? If not, why not? If so, what is the value returned by main()? Why? References, please! template <typename R> struct wat; template <typename T> struct wat <T&> { static int value(T & t) { return t * 1;…
I interactively build a simple B-tree data structure in Haskell, implementing insertion and deletion, using a GADT to enforce the structural invariant. The GADT also guides us towards a correct implementation. Also on YouTube. MP4 downloads are available from Vimeo. The slides I used for my YLJ13 talk are available in PDF or Keynote. There’s some code on GitHub, and a script.
A demonstration of a technique for using types to guide the construction of Haskell programs, based on natural deduction. Includes some tricks for getting help from the compiler, GHC. Also on YouTube. MP4 downloads are available from Vimeo. There are subtitles.