Dynamic logic is a valuable formalism that has many applications in ensuring the correctness of safety-critical systems. We present a novel theory of parameterized dynamic logic, namely \( DL _p\) , for specifying and reasoning about program models based on their operational semantics. Different from most dynamic logics that deal with regular expressions or a particular type of models, \( DL _p\) allows arbitrary forms of programs and formulas according to specific domains. It provides a language-independent proof calculus under dynamic-logic settings, supporting symbolic-execution-based reasoning with a general notion of labels for capturing program configurations. To admit certain infinite proof deductions caused by loop programs, we adapt the cyclic proof approach to the theory of \( DL _p\) by building a cyclic proof structure specific to \( DL _p\) . The soundness of \( DL _p\) is analyzed and formally proved. A case study displays an instantiation of \( DL _p\) in particular domains, demonstrating the potential usage of \( DL _p\) in program verification.