8 citations · 18 across the 4 of their papers we have counts for
4 papers
Formal Verification of Zero-Knowledge Circuits
Alessandro Coglio, Eric McCarthy, Eric W. Smith
Zero-knowledge circuits are sets of equality constraints over arithmetic expressions interpreted in a prime field; they are used to encode computations in cryptographic zero-knowle…
Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses
Ruben Gamboa, Panagiotis Manolios, Eric Smith +1
Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems, such as (REVERSE (REVERSE X)) = X. Experienced ACL2 users will recognize…
A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann, Eric W. Smith
We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old…
Polymorphic Types in ACL2
Benjamin Selfridge, Eric Smith
This paper describes a tool suite for the ACL2 programming language which incorporates certain ideas from the Hindley-Milner paradigm of functional programming (as exemplified in p…