Deductive synthesis for large-scale implementations of dynamic programming algorithms. Strives to produce cache-oblivious distributed programs using a divide-and-conquer method. Incorporates modern proof techniques with a software refinement paradigm.