Examples of interesting semantics to study during a small project for a graduate Semantics course
You could add more flow control to IMP, like (simple) exceptions, or break to exit early from a while loop.

You could some partial operators (division, square root) requiring you to handle runtime errors.

You could add more complex data types, like pairs. Make it so that e.g. projecting a value out of a non-pair value causes a runtime error. Craft a (first-order) simple type system e.g. using T ::= int | (T*T) as types, and prove that "typeable programs do not go wrong", i.e. executing them never lead to runtime errors.

You could add functions / procedures. This is not so trivial at first, especially if you want to consider several ways for parameter passing (e.g. pass-by-value, pass-by-reference).

You could prove that a suitable restriction of IMP (say, sans while, or with a constrained while) is always terminating.