Skip to main content

TS

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

BibTeX Entry

  @article{Norrish_09,
    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}
  }

Download

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