Lens as a computation structure for organizing concolic execution of a weakest precondition verifier.
Blog post: http://www.philipzucker.com/concolic-weakest-precondition-is-kind-of-like-a-lens/
Other thoughts:
- monoidal category for parallelism?
- what is up with seperation logic.