Trustworthy Systems

Rewriting conversions implemented with continuations

Authors

Michael Norrish

NICTA

Abstract

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-inefficient. An explicit representation of continuations improves performance on large terms, and on long-running computations.

BibTeX Entry

  @article{Norrish_09,
    author           = {Norrish, Michael},
    journal          = {Journal of Automated Reasoning},
    keywords         = {interactive theorem-proving, rewriting, continuations, functional programming},
    month            = oct,
    number           = {3},
    pages            = {305--336},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/1481.pdf},
    title            = {Rewriting Conversions Implemented with Continuations},
    volume           = {43},
    year             = {2009}
  }

Download