| Publication | Date of Publication | Type |
|---|
| A theorem prover for a computational logic | 2023-04-28 | Paper |
| Limited second-order functionality in a first-order setting | 2020-03-03 | Paper |
| Milestones from the Pure Lisp Theorem Prover to ACL2 | 2019-12-18 | Paper |
| A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program | 2018-07-09 | Paper |
| Machines Reasoning About Machines: 2015 | 2016-01-08 | Paper |
| Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete | 2014-09-08 | Paper |
| Rough Diamond: An Extension of Equivalence-Based Rewriting | 2014-09-08 | Paper |
| ACL2s: “The ACL2 Sedan” | 2013-12-20 | Paper |
| A fast string searching algorithm | 2011-08-31 | Paper |
| Correct Hardware Design and Verification Methods | 2010-02-05 | Paper |
| Correct Hardware Design and Verification Methods | 2010-02-05 | Paper |
| Integrating external deduction tools with ACL2 | 2009-03-25 | Paper |
| An ACL2 Tutorial | 2008-12-04 | Paper |
| Rewriting with equivalence relations in ACL2 | 2008-06-11 | Paper |
| Efficient execution in an automated reasoning environment | 2008-01-18 | Paper |
| Formal Methods in Computer-Aided Design | 2006-10-20 | Paper |
| Meta Reasoning in ACL2 | 2006-07-06 | Paper |
| Theorem Proving in Higher Order Logics | 2006-07-06 | Paper |
| Executable JVM model for analytical reasoning: A study | 2005-09-22 | Paper |
| Theorem Proving in Higher Order Logics | 2005-08-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3021914 | 2005-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4817211 | 2004-09-22 | Paper |
| Partial functions in ACL2 | 2004-03-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4790668 | 2003-02-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4551175 | 2002-09-04 | Paper |
| On the desirability of mechanizing calculational proofs | 2002-07-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2734953 | 2001-08-30 | Paper |
| Structured theory development for a mechanized logic | 2001-02-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4503919 | 2000-09-14 | Paper |
| Introduction to the OBDD algorithm for the ATP community | 1995-01-12 | Paper |
| A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol | 1994-03-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4040283 | 1993-06-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4016540 | 1993-01-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3490989 | 1990-01-01 | Paper |
| The addition of bounded quantification and partial functions to a computational logic and its theorem prover | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3835049 | 1988-01-01 | Paper |
| Proof Checking the RSA Public Key Encryption Algorithm | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3345811 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3709921 | 1984-01-01 | Paper |
| A Mechanical Proof of the Unsolvability of the Halting Problem | 1984-01-01 | Paper |
| A mechanical proof of the termination of Takeuchi's function | 1979-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3894958 | 1979-01-01 | Paper |
| Proving Theorems about LISP Functions | 1975-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5663380 | 1972-01-01 | Paper |
