Rewriting conversions implemented with continuations

Michael Norrish

doi:10.1007/s10817-009-9146-5

Rewriting conversions implemented with continuations

Michael Norrish^*

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

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.

Original language	English
Pages (from-to)	305-336
Number of pages	32
Journal	Journal of Automated Reasoning
Volume	43
Issue number	3
DOIs	https://doi.org/10.1007/s10817-009-9146-5
Publication status	Published - 2009
Externally published	Yes

Access to Document

10.1007/s10817-009-9146-5

Cite this

@article{3fd9f693c33d420ea34fa57739f8a070,

title = "Rewriting conversions implemented with continuations",

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.",

keywords = "Continuation-passing style, Interactive theorem-proving, Rewriting",

author = "Michael Norrish",

year = "2009",

doi = "10.1007/s10817-009-9146-5",

language = "English",

volume = "43",

pages = "305--336",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "3",

}

TY - JOUR

T1 - Rewriting conversions implemented with continuations

AU - Norrish, Michael

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - Continuation-passing style

KW - Interactive theorem-proving

KW - Rewriting

UR - http://www.scopus.com/inward/record.url?scp=70349590946&partnerID=8YFLogxK

U2 - 10.1007/s10817-009-9146-5

DO - 10.1007/s10817-009-9146-5

M3 - Article

SN - 0168-7433

VL - 43

SP - 305

EP - 336

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 3

ER -

Rewriting conversions implemented with continuations

Abstract

Access to Document

Other files and links

Fingerprint

Cite this