Abstract: “Algebraic denotational semantics (ADS) is our approach to describe the semantics of an imperative programming language in the order sorted equational logic. Using CafeOBJ, an algebraic specification language, the syntax of an imperative language, Minila, is specified into modules of sorts, operators and rewriting rules, and its algebraic semantics are specified by the Environment. The compiler of Minila language is also specified into a module whose rewriting rules describe the transformation from Minila programs into sequences of machine instructions. In addition, the semantics of machine language is considered to guarantee the semantics preservation of the Compiler. The main part of our research is verifying the correctness of compiler for Minila language using CafeOBJ proof assistant.”