Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy. A mechanized semantics for C++ object construction and destruction, with applications to resource management. In POPL 2012: 39th symposium Principles of Programming Languages, pages 521--532. ACM, 2012.

We present a formal operational semantics and its Coq mechanization for the C++ object model, featuring object construction and destruction, shared and repeated multiple inheritance, and virtual function call dispatch. These are key C++ language features for high-level system programming, in particular for predictable and reliable resource management. This paper is the first to present a formal mechanized account of the metatheory of construction and destruction in C++, and applications to popular programming techniques such as “resource acquisition is initialization.” We also report on irregularities and apparent contradictions in the ISO C++03 and C++11 standards.

bib | DOI | Local copy | At publisher's site ] Back

This file was generated by bibtex2html 1.99.