Awesome! I have been wanting to do something almost exactly like this for a very long time, and it looks like O’Connor did a great job. They even did the thing where you identify unapplied sub-expressions with known computations and call out to an optimized C version, although their version is more elegant than what I was thinking (calling functions by hash rather than by value).
I only recently got interested enough in blockchain to start really learning about it, reading the technical papers, etc. High on my list of problems to solve was formal verification of contracts. I think this paper knocks it out of the park, although admittedly there may be other contenders in the literature I don’t know about.
The company O’Connor is with, Blockstream, looks to me like a leader in “figuring stuff out” for blockchain. I also like their sidechains proposal, https://blockstream.com/technology/sidechains.pdf, it is not a complete solution and the paper points out several problem areas. The company is a backer of the Elements Project https://elementsproject.org/ which experiments with sidechains.
I also just found a Confidential Assets paper by people in the company, https://blockstream.com/bitcoin17-final41.pdf, I have not read yet.