The first line of the abstract reminds me of some recent work allowing plain Haskell functions to be sent to the Z3 theorem prover/SMT program:

http://newartisans.com/2017/04/haskell-and-z3/

It leverages some cool work of Conal Elliott that develops (formulas in) cartesian closed categories into something like an "intermediate representation" for functional language compilation.

http://conal.net/blog/posts/haskell-to-hardware-via-cccs http://conal.net/blog/posts/overloading-lambda

http://conal.net/papers/compiling-to-categories/ (the "LaTeX goals" ICFP 2017 paper)

--

Also, something I always like to link when this kind of thing comes up: the salamander lemma!

https://sbseminar.wordpress.com/2007/11/13/anton-geraschenko...

https://mathoverflow.net/questions/6749/a-proof-of-the-salam...