Core Erlang is a subset and intermediate representation of the Erlang programming language; as such, it shares Erlang's characteristic features, such as the absence of partial function application, strict evaluation, dynamic typing, and asynchronous communication between concurrently running processes. In this research, we examine the sequential sublanguage of Core Erlang using various formal semantics definitional styles (small-step and big-step approaches) and define the semantics of concurrent Core Erlang using a small-step approach. The scope of this research includes the evaluation and comparison of these definitions, as well as the applications of different semantics (such as proving program correctness). Among these applications, the investigation of program equivalence is particularly noteworthy, serving as a basis for verifying the correctness of program transformations (e.g., refactorings and optimizations). The research results are also formalised in the Rocq proof assistant.