Relating models of backtracking
Mitchell Wand, Dale Vaillancourt · ACM SIGPLAN Notices · 2004
Past attempts to relate two well-known models of backtracking computation have met with only limited success. We relate these two models using logical relations. We accommodate higher-order values and infinite computations. We also provide an operational semantics, and we prove it adequate for both models.