C++.T Formalization in Isar
Author
Siek, Jeremy G.; Taha, Walid
Date
December 16, 2005Abstract
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.
Citation
Type
Technical report