ACL2: an industrial strength version of Nqthm
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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.Keywords
This publication has 17 references indexed in Scilit:
- A Ramsey theorem in Boyer-Moore logicJournal of Automated Reasoning, 1995
- Metamathematics, Machines and Gödel's ProofPublished by Cambridge University Press (CUP) ,1994
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocolFormal Aspects of Computing, 1994
- Introduction to the OBDD algorithm for the ATP communityJournal of Automated Reasoning, 1994
- An extension of the Boyer-Moore Theorem Prover to support first-order quantificationJournal of Automated Reasoning, 1992
- Machine checked proofs of the design of a fault-tolerant circuitFormal Aspects of Computing, 1992
- A formal HDL and its use in the FM9001 verificationPhilosophical Transactions A, 1992
- A mechanical proof of Quadratic ReciprocityJournal of Automated Reasoning, 1992
- Textbook Examples of RecursionPublished by Elsevier ,1991
- A mechanical proof of the Church-Rosser theoremJournal of the ACM, 1988