Rewriting Conversions Implemented with Continuations

Select |




Print


Norrish, Michael

Norrish, Michael


2009-10-01


Journal Article


Journal of Automated Reasoning (JAR)


43


3


305-336


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.


Interactive theorem-proving, rewriting, continuations, functional programming


http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s10817-009-9146-5


nicta:1481


Norrish, Michael. Rewriting Conversions Implemented with Continuations. Journal of Automated Reasoning (JAR). 2009-10-01; 43(3):305-336.



Loading citation data...

Citation counts
(Requires subscription to view)