For families of related software programs, it can be convenient to
implement libraries of generic algorithms, which can be proved
once; and then specialize those algorithms to parameters and
optimize the new less-general programs.  If the latter process is
also verified, we have an appealing recipe for churning out
verified code quickly.  One use case that the MIT subteam works on
is generating low-level code for cryptographic primitives, which
are often parameterized on large prime numbers.  Our original
approach to partial evaluation (a term of art for compile-time
optimization of function specializations) was to use Coq's
built-in term reduction.  However, we do not want full reduction
to normal forms, since variables standing for runtime inputs
remain in the output; and telling Coq about a customized reduction
strategy is too difficult, when we don't want to wait for hours or
more for a reduction to finish, as we encountered for quite a few
parameter sets.  I will explain the alternative strategy we have
developed, which is essentially a new low-trusted-code-base
approach to fast, customized reduction and rewriting in Coq,
combining the ideas of proof by reflection, parametric
higher-order abstract syntax, normalization by evaluation, and
efficient compilation of pattern matches.