Iteration in ACL2
Logic in Computer Science
2020-09-30 v1 Symbolic Computation
Abstract
Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- provides direct support for iteration. We describe an ACL2 analogue loop$ of loop that supports efficient ACL2 programming and reasoning with iteration.
Cite
@article{arxiv.2009.13762,
title = {Iteration in ACL2},
author = {Matt Kaufmann and J Strother Moore},
journal= {arXiv preprint arXiv:2009.13762},
year = {2020}
}
Comments
In Proceedings ACL2 2020, arXiv:2009.12521