An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++

We present an operational semantics and type safety proof for multiple inheritance in C++.The semantics models the behavior of method calls, field accesses, and two forms of casts in C++ class hierarchies exactly, and the type safety proof was formalized and machine-checked in Isabelle/HOL. Our semantics enables one, for the first time, to understand the behavior of operations on C++ class hierarchies without referring to implementation-level artifacts such as virtual function tables. Moreover, it can as the semantics is executable-act as a reference for compilers, and it can form the basis for more advanced correctness proofs of, e.g., automated program transformations. The paper presents the semantics and type safety proof, and a discussion of the many
subtleties that we encountered in modeling the intricate multiple inheritance model of C++.