A mechanized semantics for C++ object construction and destruction, with applications to resource management

DOI10.1145/2103656.2103718MaRDI QIDQ2942898zbMATH OpenOpenAlexFDO

Authors Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy

Publication date 11 September 2015

Published in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00674663/file/cpp-construction.pdf

zbMATH Keywords

CoqC++classesobjectsmechanized semanticsconstructorsdestructors

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 868106
• A principled, complete, and efficient representation of C++
• A Fully Abstract Semantics for Constructor Systems
• scientific article; zbMATH DE number 804369
• A CuCh interpretation of an object-oriented language
• Mechanized semantics for the clight subset of the C language
• scientific article; zbMATH DE number 1002575
• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation

Cited in

(2)

• Formal verification of object layout for C++ multiple inheritance
• Verification of the ROS NavFn planner using executable specification languages

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A mechanized semantics for C++ object construction and destruction, with applications to resource management

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942898)