We present an implementation and verification in higher-order logic of Cooper’s quantifier elimination for Presburger arithmetic.
Reflection, i.e. the direct execution in ML, yields a speed-up of a factor of 200 over an LCF-style implementation and performs
as well as a decision procedure hand-coded in ML.