K  is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Isabelle/HOL  is a generic proof engine which allows mathematical formulas to be built into a formal language and provides tools to prove those formulas in a logical calculus. In this paper we define IsaK, a reference semantics for K, which was developed through discussions with the K team to meet their expectations for a semantics for K. Previously, we defined the static semantics for K ; thus, this paper mainly focuses on its dynamic semantics. More importantly, we investigate a way to connect K and Isabelle by building a translation framework, TransK, to translate programming languages defined in K into theories defined in Isabelle, which can not only allow programmers to define their programming languages easily in K but also have the ability to reason about their languages in Isabelle. In order to show a well-established translation, we prove that the K specification is sound and relatively complete with respect to the translated Isabelle theory by TransK. To the best of our knowledge, IsaK is the first complete formal semantics defined for K, while TransK is the first complete translation from a real-world, order-sorted algebraic system to a many-sorted one. All the work is formalized in Isabelle/HOL at https://github.com/liyili2/KtoIsabelle.