C++.T Formalization in Isar

Thumbnail
Name:
TR05-458.pdf
Size:
163.0Kb
Format:
PDF
View/Open
Author
Siek, Jeremy G.; Taha, Walid
Date
December 16, 2005
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.
Citation
Siek, Jeremy G. and Taha, Walid. "C++.T Formalization in Isar." (2005) https://hdl.handle.net/1911/96344.
Type
Technical report
Citable link to this page
https://hdl.handle.net/1911/96344
Rights
You are granted permission for the noncommercial reproduction, distribution, display, and performance of this technical report in any format, but this permission is only for a period of forty-five (45) days from the most recent time that you verified that this technical report is still available from the Computer Science Department of Rice University under terms that include this permission. All other rights are reserved by the author(s).
Metadata
Show full item record
Collections