Complexity certification of C++ template metaprogramming (extended version)

Any partial recursive function can be computed at compile time, using C++ templates to define primitive recursion, composition, and minimalization. In this paper, we define a restricted language based on C++ templates, and we prove that it characterizes the set of polynomial-time computable functions, that is the set of functions computed by a Turing machine with time bounded by a polynomial