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

Research Paper

Thursday, Oct 26, from 13:30 to 15:00

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++.