| Publication | Date of Publication | Type |
|---|
| Iteration in ACL2 | 2024-08-22 | Paper |
| How can I do that with ACL2? Recent enhancements to ACL2 | 2024-08-13 | Paper |
| Enhancements to ACL2 in versions 5.0, 6.0, and 6.1 | 2024-08-13 | Paper |
| A theorem prover for a computational logic | 2023-04-28 | Paper |
Limited second-order functionality in a first-order setting
Journal of Automated Reasoning | 2020-03-03 | Paper |
Milestones from the Pure Lisp Theorem Prover to ACL2
Formal Aspects of Computing | 2019-12-18 | Paper |
A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
IEEE Transactions on Computers | 2018-07-09 | Paper |
Machines Reasoning About Machines: 2015
Automated Technology for Verification and Analysis | 2016-01-08 | Paper |
Rough diamond: an extension of equivalence-based rewriting
Interactive Theorem Proving | 2014-09-08 | Paper |
Proof pearl: proving a simple von Neumann machine Turing complete
Interactive Theorem Proving | 2014-09-08 | Paper |
ACL2s: ``the ACL2 sedan
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
A fast string searching algorithm
Communications of the ACM | 2011-08-31 | Paper |
Linear and nonlinear arithmetic in ACL2
Lecture Notes in Computer Science | 2010-02-05 | Paper |
Inductive assertions and operational semantics
Lecture Notes in Computer Science | 2010-02-05 | Paper |
Integrating external deduction tools with ACL2
Journal of Applied Logic | 2009-03-25 | Paper |
An ACL2 Tutorial
Lecture Notes in Computer Science | 2008-12-04 | Paper |
Rewriting with equivalence relations in ACL2
Journal of Automated Reasoning | 2008-06-11 | Paper |
Efficient execution in an automated reasoning environment
Journal of Functional Programming | 2008-01-18 | Paper |
Formal Methods in Computer-Aided Design
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Meta Reasoning in ACL2
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Executable JVM model for analytical reasoning: A study
Science of Computer Programming | 2005-09-22 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2005-08-18 | Paper |
| scientific article; zbMATH DE number 2177632 (Why is no real title available?) | 2005-06-21 | Paper |
| scientific article; zbMATH DE number 2101985 (Why is no real title available?) | 2004-09-22 | Paper |
Partial functions in ACL2
Journal of Automated Reasoning | 2004-03-15 | Paper |
| scientific article; zbMATH DE number 1863393 (Why is no real title available?) | 2003-02-04 | Paper |
| scientific article; zbMATH DE number 1796151 (Why is no real title available?) | 2002-09-04 | Paper |
On the desirability of mechanizing calculational proofs
Information Processing Letters | 2002-07-25 | Paper |
| Towards a mechanically checked theory of computation. The ACL2 project | 2001-08-30 | Paper |
Structured theory development for a mechanized logic
Journal of Automated Reasoning | 2001-02-18 | Paper |
| scientific article; zbMATH DE number 1507199 (Why is no real title available?) | 2000-09-14 | Paper |
Introduction to the OBDD algorithm for the ATP community
Journal of Automated Reasoning | 1995-01-12 | Paper |
A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
Formal Aspects of Computing | 1994-03-27 | Paper |
| scientific article; zbMATH DE number 193479 (Why is no real title available?) | 1993-06-05 | Paper |
| scientific article; zbMATH DE number 88983 (Why is no real title available?) | 1993-01-16 | Paper |
| scientific article; zbMATH DE number 4164171 (Why is no real title available?) | 1990-01-01 | Paper |
The addition of bounded quantification and partial functions to a computational logic and its theorem prover
Journal of Automated Reasoning | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4112064 (Why is no real title available?) | 1988-01-01 | Paper |
A Mechanical Proof of the Unsolvability of the Halting Problem
Journal of the ACM | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3880145 (Why is no real title available?) | 1984-01-01 | Paper |
Proof Checking the RSA Public Key Encryption Algorithm
The American Mathematical Monthly | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3938596 (Why is no real title available?) | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3702108 (Why is no real title available?) | 1979-01-01 | Paper |
A mechanical proof of the termination of Takeuchi's function
Information Processing Letters | 1979-01-01 | Paper |
Proving Theorems about LISP Functions
Journal of the ACM | 1975-01-01 | Paper |
| scientific article; zbMATH DE number 3395362 (Why is no real title available?) | 1972-01-01 | Paper |
