mlsanityData to 14 Oct 2026

Iteration in ACL2

arXiv 2009.13762 ↗First posted 29 Sep 2020cs.LO cs.SCcited by 1

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). First posted on arXiv 29 Sep 2020.

Builds on

No reference list yet.

Built on by

Cited by year

Citing papers per year: 2023: 1.

1 paper.

  1. 2023Advances in ACL2 Proof Debugging Toolscited by 0