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.
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.
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.
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.
This post is an extended version of a lightning talk I gave at the Brisbane
Functional Programming Group. It introduces the differencelist, 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 intermediates.
Here’s a little exercise for anyone who, like me, recently came across
ScottMeyers’ work on universalreferences 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!
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 Clang3.3 and GCC4.8.1 don’t even agree on this program, so there’s not
much point in cheating!
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.