Complexity certification of C++ template metaprogramming

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