Abstract is missing.
- A verifying core for a cryptographic language compilerLee Pike, Mark Shields, John Matthews. 1-10 [doi]
- A robust machine code proof framework for highly secure applicationsDavid S. Hardin, Eric W. Smith, William D. Young. 11-20 [doi]
- Unique factorization in ACL2: Euclidean domainsJohn R. Cowles, Ruben Gamboa. 21-27 [doi]
- Parameterized congruences in ACL2David Greve. 28-34 [doi]
- Soundness of the simply typed lambda calculus in ACL2Sol Swords, William R. Cook. 35-39 [doi]
- An embedding of the ACL2 logic in HOLMichael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds. 40-46 [doi]
- Towards a formal theory of on chip communications in the ACL2 logicJulien Schmaltz, Dominique Borrione. 47-56 [doi]
- Memories: array-like records for ACL2Jared Davis. 57-60 [doi]
- The ideal of verified softwareTony Hoare. 61-62 [doi]
- Combining ACL2 and an automated verification tool to verify a multiplierErik Reeber, Jun Sawada. 63-70 [doi]
- Implementing a cost-aware evaluator for ACL2 expressionsRuben Gamboa, John R. Cowles. 71-80 [doi]
- Function memoization and unique object representation for ACL2 functionsRobert S. Boyer, Warren A. Hunt Jr.. 81-89 [doi]
- Adding parallelism capabilities to ACL2David L. Rager. 90-94 [doi]
- Quantification in tail-recursive function definitionsSandip Ray. 95-98 [doi]
- Phylogenetic trees in ACL2Warren A. Hunt Jr., Serita M. Nelesen. 99-102 [doi]
- Double rewriting for equivalential reasoning in ACL2Matt Kaufmann, J. Strother Moore. 103-106 [doi]
- ACL2 in DrSchemeDale Vaillancourt, Rex L. Page, Matthias Felleisen. 107-116 [doi]
- Reasoning about ACL2 file inputJared Davis. 117-126 [doi]
- A SAT-based procedure for verifying finite state machines in ACL2Warren A. Hunt Jr., Erik Reeber. 127-135 [doi]