- Mertcan Temel
:
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2. ACL2 2020: 61-74 - Ruben Gamboa, John R. Cowles, Woodrow Gamboa:
Quadratic Extensions in ACL2. ACL2 2020: 75-86 - Sol Swords:
Generating Mutually Inductive Theorems from Concise Descriptions. ACL2 2020: 95-107 - Alessandro Coglio:
Ethereum's Recursive Length Prefix in ACL2. ACL2 2020: 108-124 - Alessandro Coglio, Stephen J. Westfold:
Isomorphic Data Type Transformations. ACL2 2020: 125-141 - Grant O. Passmore, Ruben Gamboa:
Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020. EPTCS 327, 2020 [contents] - 2018
- Alessandro Coglio:
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. ACL2 2018: 1-17 - Mihir Parang Mehta:
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32. ACL2 2018: 18-29 - David A. Greve, Andrew Gacek:
Trapezoidal Generalization over Linear Constraints. ACL2 2018: 30-46 - Sol Swords:
Incremental SAT Library Integration Using Abstract Stobjs. ACL2 2018: 47-60 - David S. Hardin, Konrad Slind:
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems. ACL2 2018: 61-76 - Alessandro Coglio, Shilpi Goel:
Adding 32-bit Mode to the ACL2 Model of the x86 ISA. ACL2 2018: 77-94 - Ruben Gamboa, John R. Cowles:
The Fundamental Theorem of Algebra in ACL2. ACL2 2018: 98-110 - Carl Kwan, Mark R. Greenstreet:
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r). ACL2 2018: 111-127 - Carl Kwan, Mark R. Greenstreet:
Convex Functions in ACL2(r). ACL2 2018: 128-142 - Yan Peng, Mark R. Greenstreet:
Smtlink 2.0. ACL2 2018: 143-160 - Sol Swords:
Hint Orchestration Using ACL2's Simplifier. ACL2 2018: 164-171 - Matt Kaufmann:
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract). ACL2 2018: 161-163 - Shilpi Goel, Matt Kaufmann:
Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018. EPTCS 280, 2018 [contents] - 2017
- Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith:
A Versatile, Sound Tool for Simplifying Definitions. ACL2 2017: 61-77 - John R. Cowles, Ruben Gamboa:
The Cayley-Dickson Construction in ACL2. ACL2 2017: 18-29 - Shilpi Goel:
The x86isa Books: Features, Usage, and Future Plans. ACL2 2017: 1-17 - Matt Kaufmann, Sol Swords:
Meta-extract: Using Existing Facts in Meta-reasoning. ACL2 2017: 47-60 - David M. Russinoff:
A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve. ACL2 2017: 30-46 - Rob Sumners:
Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications. ACL2 2017: 78-94 - Sol Swords:
Term-Level Reasoning in Support of Bit-blasting. ACL2 2017: 95-111 - Anna Slobodová, Warren A. Hunt Jr.:
Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017. EPTCS 249, 2017 [contents] - 2015
- Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.:
Fourier Series Formalization in ACL2(r). ACL2 2015: 35-51 - Alessandro Coglio:
Second-Order Functions and Theorems in ACL2. ACL2 2015: 17-33 - John R. Cowles, Ruben Gamboa:
Perfect Numbers in ACL2. ACL2 2015: 53-59
