4 citations · 4 across the 1 of their papers we have counts for
3 papers
cs.LO2020★ 4 cited
Iteration in ACL2
Matt Kaufmann, J Strother Moore
Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- pro…
cs.PL2017
A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann, Eric W. Smith
We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old…
cs.LO2017
Meta-extract: Using Existing Facts in Meta-reasoning
Matt Kaufmann, Sol Swords
ACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class :meta or :clause-processor ar…