### 13 papers:

- TACAS-2011-ChamarthiDMV #proving #theorem proving
- The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.
- LOPSTR-2010-HerasPR #correctness #proving #set
- Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System (JH, VP, JR), pp. 37–51.
- ICEIS-ISAS-2009-HidalgoGT #consistency #data type #detection #nondeterminism #performance
- Efficient Data Structures for Local Inconsistency Detection in Firewall ACL Updates (SPH, RMG, FTdlR), pp. 176–181.
- PPDP-2009-EastlundF #composition #induction
- Making induction manifest in modular ACL2 (CE, MF), pp. 105–116.
- PADL-2009-EastlundF #towards
- Toward a Practical Module System for ACL2 (CE, MF), pp. 46–60.
- IJCAR-2006-ReeberH #satisfiability #subclass
- A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) (ER, WAHJ), pp. 453–467.
- LOPSTR-2003-Ruiz-ReinaJHM #case study #data type #performance #reasoning
- Formal Reasoning about Efficient Data Structures: A Case Study in ACL2 (JLRR, JAAJ, MJH, FJMM), pp. 75–91.
- LOPSTR-2002-Martin-MateosAHR #framework #verification
- Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers (FJMM, JAA, MJH, JLRR), pp. 182–198.
- PADL-2002-BoyerM #thread
- Single-Threaded Objects in ACL2 (RSB, JSM), pp. 9–27.
- CADE-1998-Kaufmann #verification
- ACL2 Support for Verification Projects (Invited Talk) (MK), pp. 220–238.
- CAV-1998-Moore #proving
- An ACL2 Proof of Write Invalidate Cache Coherence (JSM), pp. 29–38.
- SEKE-1996-Balmas #concept #named #programming
- ACL: a Tool for Conceptual Programming (FB), pp. 198–205.
- ILPS-1993-KobayashiY #concurrent #linear #logic programming #named #paradigm
- ACL — A Concurrent Linear Logic Programming Paradigm (NK, AY), pp. 279–294.