Iteration in ACL2
Copyright policy )Iteration in ACL2
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.
In Proceedings ACL2 2020, arXiv:2009.12521
- The University of Texas at Austin United States
Computer Science - Symbolic Computation, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Symbolic Computation (cs.SC), Logic in Computer Science (cs.LO)
Computer Science - Symbolic Computation, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Symbolic Computation (cs.SC), Logic in Computer Science (cs.LO)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).4 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!