Trustworthy Systems

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

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