The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
ACL2 ("A Computational Logic for Applicative Common Lisp") is a reimplemented extended version of Boyer and Moore's (1979, 1988) Nqthm and Kaufmann's (1988, 1990, 1992) Pc-Nqthm, intended for large-scale verification projects. However, the logic supported by ACL2 is compatible with the applicative subset of Common Lisp. The decision to use an "industrial strength" programming language as the foundation of the mathematical logic is crucial to our advocacy of ACL2 in the application of formal methods to large systems. However, one of the key reasons Nqthm has been so successful, we believe, is its insistence that functions be total. Common Lisp functions are not total and this is one of the reasons Common Lisp is so efficient. This paper explains how we scaled up Nqthm's logic to Common Lisp, preserving the use of total functions within the logic but achieving Common Lisp execution speeds.
@misc{kaufmann1996acl2,
title = {ACL2: an industrial strength version of Nqthm},
author = {Matt Kaufmann and J Strother Moore},
year = {1996},
pages = {23--34},
doi = {10.1109/cmpass.1996.507872},
}
This record lives at https://refs.drheap.org/kaufmann1996acl2/ and will keep
doing so. It used to be called kaufmann2002acl2, and those addresses still resolve to this one.