On Tuesday my colleagues and I were invited by Christine Rizkallah, who has very graciously been acting as a host for us at Melbourne Connect, to attend a session of the [Programming Languages and Verification Reading Group][1] organised by V. Jackson.
The paper of interest this week was [A Marriage of Rely/Guarantee and Separation Logic][2], by Viktor Vafeiadis & Matthew Parkinson, and the two
[Regular-expression derivatives re-examined][1] was the paper for the Programming Languages and Verification Reading Group this week, unfortunately I wasn't able to attend but I went through it by myself and thankfully understood most of it as it's a clear introduction to a topic I have spent some time on in the past.
Back in 2008 I implemented Brzozowski derivatives in Coq, which was quite fun (see attached file basic.v). It describes regular expression semantics and proves that a regexp matches a string if repeatedly taking the derivative for each character in the string results in a nullable regexp. (I didn't implement automata construction as I had other plans for that).
For an additional challenge I implemented logical and/intersection and also an "interleave" operator allowing two regular expressions to be combined into one that matches every possible interleaving of the strings that each match (see attached file extended.v).
I wasn't able to successfully prove the correctness of derivatives with not
After missing a couple of sessions I was able to attend the reading group to go through [There and back again][1], a functional pearl demonstrating techniques for recursing over a list or other data structure and processing it "at return time" to perform convolutions or other operations like palindrome checking.
The examples were all given in ML which gives me a bit of a headache, but the paper leads off with three exercises for the reader that were very helpful for focusing the attention and led to some interesting discussion.
The attached files demonstrate how to use the there-and-back-again approach in Haskell (taba.hs) and Prolog (taba.pl) to implement convolution, palindrome checking, and also general list reverse. It's basically just using the call stack to avoid needing to construct an auxiliary list, and whether that's beneficial or not depends on what you're doing (and how big is your