Rewriting Conversions Implemented with Continuations
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.
|Collections||ANU Research Publications|
|Source:||Journal of Automated Reasoning|
|01_Norrish_Rewriting_Conversions_2009.pdf||221.66 kB||Adobe PDF||Request a copy|
|02_Norrish_Rewriting_Conversions_2009.pdf||347.03 kB||Adobe PDF||Request a copy|
|03_Norrish_Rewriting_Conversions_2009.pdf||10.49 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.