Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce <i>Heterogeneous Dynamic Logic</i> (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their calculi, are treated as <i>dynamic theories</i> that can be combined to reason about heterogeneous systems whose components are verified using different program logics. HDL provides two key operations: <i>Lifting</i> extends an individual dynamic theory with new program constructs (e.g., the havoc operation or regular programs) and automatically augments its calculus with sound reasoning principles for the new constructs; and <i>Combination</i> enables cross-language reasoning in a <i>single modality</i> via <i>Heterogeneous Dynamic Theories</i>, facilitating the reuse of existing proof infrastructure. By lifting combined theories with regular programs, we obtain <i>heterogeneous</i> control structures that allow us to reason about intertwined cross-language behavior. We formalize dynamic theories, their lifting and combination, and prove the soundness of all proof rules in Isabelle. We also introduce a proof rule combining deductive DL-based reasoning with reasoning principles from Kleene Algebras with Tests. Furthermore, we prove <i>relative completeness</i> theorems for lifting and combination: Under usual assumptions, reasoning about lifted or combined theories is no harder than reasoning about the constituent dynamic theories and their common first-order structure (i.e., the data theory). We demonstrate HDL's value by verifying an automotive case study where a Java controller (formalized in Java dynamic logic) steers a plant model (formalized in differential dynamic logic).