ACL2 Workshop 2020 Program

ACL2 Workshop 2020 Program

Accepted Papers

  • Matt Kaufmann and J Moore. Iteration in ACL2.
  • Ruben Gamboa, John Cowles and Woodrow Gamboa. Quadratic Extensions in ACL2.
  • Sol Swords. New Rewriter Features in FGL.
  • Sol Swords. Generating Mutually Inductive Theorems from Concise Descriptions.
  • Rob Sumners. Computing and Proving Well-founded Orderings through Finite Abstractions.
  • David Greve. Minimal fractional representations of integers mod M.
  • Carl Kwan, Yan Peng and Mark R. Greenstreet. Cauchy-Schwarz for ACL2 Abstract Vector Spaces.
  • Alessandro Coglio. Ethereum's Recursive Length Prefix in ACL2.
  • Yan Peng and Mark Greenstreet. Type Inference Using Meta-extract for Smtlink and Beyond.
  • Mertcan Temel. RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2.
  • David Hardin. Put Me on the RAC.
  • Alessandro Coglio and Stephen Westfold. Isomorphic Data Type Transformations.