8 citations · 18 across the 4 of their papers we have counts for
3 papers · 1 filter
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…
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…