Design of Semantics by Abstract Interpretation

expressed in fixpoint form, we derive, by successive Galois
connection based abstract interpretations, a hierarchy of semantics
including a big-step semantics, natural, demoniac and angelic
relational semantics and equivalent nondeterministic denotational
semantics, D. Scott's deterministic denotational semantics,
generalized/conservative/liberal predicate transformer semantics,
generalized/total/partial correctness axiomatic semantics and
corresponding proof methods.