## In praise of scatter plots

A lot of papers include a graph that benchmarks the performance of a new technique against a technique from previous work. Such a graph might look like this: The graph is rather straightforward to read: when the green bar is higher, the old technique is faster, and when the red bar is higher, the new… Continue reading In praise of scatter plots

## The Isabelle logo as end-of-proof symbol

In a recent research paper, I formalised some of my theorems in the proof assistant Isabelle, but left some of them as just proved 'by hand'. I found it helpful to use a different 'QED' symbol depending on which method I had used. Below is an enlarged version of the 'three cubes' symbol in the snippet… Continue reading The Isabelle logo as end-of-proof symbol

## A star operator for functions

If $latex f$ and $latex g$ are functions, what does $latex f*g$ mean? Definition 1. A separation algebra (citation) is a triple $latex (M, \circ, u)$, where $latex M$ is a set, $latex \circ$ has type $latex M \times M \rightharpoonup M$ and is commutative, associative and cancellative, and $latex u\in M$ is the unit… Continue reading A star operator for functions