I’ve been collecting resources for automating verification and/or synthesis of programs. Although plenty exist for data, there’s a lot less for control flow. They usually need some clean or at least precise way to specify it that a mechanical translation handles from there. I’m surprised I haven’t seen recursion schemes before this post since it superficially looks like it would help there. Maybe it could be built on CakeML or something.
I’ve been collecting resources for automating verification and/or synthesis of programs. Although plenty exist for data, there’s a lot less for control flow. They usually need some clean or at least precise way to specify it that a mechanical translation handles from there. I’m surprised I haven’t seen recursion schemes before this post since it superficially looks like it would help there. Maybe it could be built on CakeML or something.
Have you read Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire? I guess you might be interested in a more lang-neutral formalism of this same concept.
Thanks for the link. :)
This may also be helpful while going through that paper: http://blog.ezyang.com/2010/05/bananas-lenses-envelopes-and-barbed-wire-a-translation-guide/
(Although, it brings it back into the Haskell domain, but still may be more comprehensible than some of the notation in that paper…)