Journal of Automated Reasoning manuscript No. (will be inserted by the editor) Rewriting Conversions Implemented with Continuations

the date of receipt and acceptance should be inserted later Abstract We give a continuation-based implementation of rewriting for systems in the LCF tradition. These systems must construct explicit proofs of equations when rewriting, and currently do so in a way that can be very space-inefficient. An explicit representation of continuations improves performance on large terms, and on long-running computations.