C++.T Formalization in Isar
Siek, Jeremy G.
A formal account of C++ templates, including the compile-time and run-time semantics. The main result is a proof of type safety. The proof is written in the Isar proof language and can be mechanically verified using the Isabelle 2005 proof assistant.