Meta Reasoning in ACL2
From MaRDI portal
Publication:5477654
DOI10.1007/11541868_11zbMath1152.68522OpenAlexW1490999085MaRDI QIDQ5477654
Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith, Warren A. jun. Hunt
Publication date: 6 July 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11541868_11
Related Items (7)
The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Directly reflective meta-programming ⋮ An ACL2 Tutorial ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ A graph library for Isabelle ⋮ Second-Order Programs with Preconditions ⋮ Integrating external deduction tools with ACL2
Uses Software
This page was built for publication: Meta Reasoning in ACL2