Deductive synthesis for large-scale implementations of dynamic programming algorithms
Strives to produce cache-oblivious distributed programs using a divide-and-conquer method. The project incorporates modern proof techniques with a software refinement paradigm, into an interactive setting that promotes cooperation between the human programmer and the compiler.
