Skip to main content


Rewriting conversions implemented with continuations


Michael Norrish



We give an 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-inef´Čücient. An explicit representation of continuations improves performance on large terms, and on long-running computations.

BibTeX Entry

    journal          = {Journal of Automated Reasoning},
    author           = {Norrish, Michael},
    number           = {3},
    month            = oct,
    volume           = {43},
    year             = {2009},
    keywords         = {interactive theorem-proving, rewriting, continuations, functional programming},
    title            = {Rewriting Conversions Implemented with Continuations},
    pages            = {305-336}


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.