Abstract
We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference — the latter being a variant of Nelson’s biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non-monotonic program combinators.
Related
Computer Scientist
My research interests include software reliability, software verification, and formal methods applied to software engineering. I am also interested in interactive storytelling. For more details, see some of my projects or my selected (or recent) publications. More posts are available in my blog. Follow me on Twitter or add me on LinkedIn.