C++.T Formalization in Isar

Thumbnail
Name:
TR05-458.pdf
Size:
163.0Kb
Format:
PDF
View/Open
Author
Siek, Jeremy G.
Taha, Walid
Date
2005-12-16
Citation
Siek, Jeremy G. and Taha, Walid. "C++.T Formalization in Isar." (2005) http://hdl.handle.net/1911/96344.
Abstract
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.
Type
Technical report
Citable link to this page
http://hdl.handle.net/1911/96344
Metadata
Show full item record
Collections