Parametric linear arithmetic over ordered fields in Isabelle/HOL

We use higher-order logic to verify a quantifier elimination procedure for linear arithmetic over ordered fields, where the coefficients of variables are multivariate polynomials over another set of variables, we call parameters. The procedure generalizes Ferrante and Rackoff's algorithm for the non-parametric case. The formalization is based on axiomatic type classes and automatically carries over to e.g. the rational, real and non-standard real numbers. It is executable, can be applied to HOL formulae and performs well or) practical examples.