Introduction to the seL4 integrity theorems

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 available in PDF and Keynote.

Also on YouTube. MP4 downloads are available from Vimeo. There are slides in PDF and Keynote.

Introduction to the seL4 proofs

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 software verification or interactive theorem proving.

Also on YouTube. MP4 downloads are available from Vimeo. There are slides, and a rough transcript.

Pattern-matching dependent types in Coq

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 techniques described by Adam Chlipala in his book, Certified Programming with Dependent Types.

We first review what it means to pattern-match on inductive families, contrasting Coq with Agda, and examine what it is about Coq that complicates pattern matching. Using a simple running example, we’ll show how to use Coq match annotations to eliminate nonsense cases, and the convoy pattern for refining the types of things already in scope. Finally, we’ll show that by equipping an inductive family with some well-chosen combinators, it is often possible to regain some semblance of elegance.

This is a recording of a practice run for a talk at YOW! Lambda Jam. You can download the video as MP4 from Vimeo. There are slides, and some code on GitHub. Also on YouTube.

C++11 universal reference pop-quiz

Here’s a little exercise for anyone who, like me, recently came across Scott Meyerswork 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; }
};

template <typename T>
struct wat <T&&> {
  static int value(T && t) { return t * 3; }
};

template <typename T>
struct ref {
  ref(T && t) : t(static_cast<T&&>(t)) {}
  int value() { return wat<T&&>::value(static_cast<T&&>(t)); }
  T && t;
};

template <typename T>
ref<T> uni(T && t) {
  return ref<T>(static_cast<T&&>(t));
}

int main() {
  int i(3);
  return uni(i).value() + uni(13).value();
}

I have written the program so that it needs no #include directives, and therefore you can be sure there is not a single typedef, decltype or auto specifier anywhere in or out of sight. That means there’s only one way that so-called universal references can arise.

However, you might find one or two other little surprises. Oh, and Clang 3.3 and GCC 4.8.1 don’t even agree on this program, so there’s not much point in cheating!

Hole-driven Haskell

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.