  We present a small-step, frame stack style, semantics for sequential Core
Erlang, a dynamically typed, impure functional programming language. The
semantics and the properties that we prove are machine-checked with the Coq
proof assistant. We improve on previous work by including exceptions and
exception handling, as well as built-in data types and functions. Based on the
semantics, we define multiple concepts of program equivalence (contextual, CIU
equivalence, and equivalence based on logical relations) and prove that the
definitions are all equivalent. Using this we are able to give a correctness
criterion for refactorings by means of contextually equivalent symbolic
expression pairs, which is one of the main motivations of this work.
