Functional programming is great, and I'm a huge fan -- but is there any interesting work on representing imperative languages categorically? Everyone and their grandma apparently knows that the simply-typed lambda calculus is the internal language of cartesian closed categories, but what about something like a simple Forth? I haven't had much luck looking for material on the semantics and theory of Forth, so I assume I've been looking in the wrong places (or using the wrong keywords).