Joseph Goguen's book [Algebraic Semantics of Imperative Programs]( is "a self-contained and novel 'executable' introduction to formal reasoning about imperative programs." The author [writes]( that it "does not explicitly use category theory, but almost everything in it was inspired in one way or another by category theory."

Goguen's homepage has more about the [OBJ language family]( (and a lot of other very interesting topics).