Fast Reflexive Arithmetic Tactics the Linear Case and Beyond

This publication has 17 references indexed in Scilit:

• Proof-carrying code from certified abstract interpretation and fixpoint compression
  Theoretical Computer Science, 2006
• A Computational Approach to Pocklington Certificates in Type Theory
  Lecture Notes in Computer Science, 2006
• Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants
  2006
• Extracting a data flow analyser in constructive logic
  Theoretical Computer Science, 2005
• Proving Equalities in a Commutative Ring Done Right in Coq
  2005
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
  Lecture Notes in Computer Science, 2005
• Interactive Theorem Proving and Program Development
  2004
• CSDP 2.3 user's guide
  Optimization Methods and Software, 1999
• A Skeptic's Approach to Combining HOL and Maple
  Journal of Automated Reasoning, 1998
• On a routing problem
  Quarterly of Applied Mathematics, 1958