Using reflection to build efficient and certified decision procedures

This publication has 6 references indexed in Scilit:

• Computational metatheory in Nuprl
  Published by Springer Nature ,2005
• Stålmarck’s algorithm as a HOL derived rule
  Published by Springer Nature ,1996
• Extending the HOL theorem prover with a computer algebra system to reason about the reals
  Published by Springer Nature ,1994
• The calculus of constructions
  Information and Computation, 1988
• Prolegomena to a theory of mechanized formal reasoning
  Artificial Intelligence, 1980
• A Catalogue of Canonical Term Rewriting Systems.
  Published by Defense Technical Information Center (DTIC) ,1980