  This document describes the implementation in SML of the LoopW language, an
imperative language with higher-order procedural variables and non-local jumps
equiped with a program logic. It includes the user manual along with some
implementation notes and many examples of certified imperative programs. As a
concluding example, we show the certification of an imperative program encoding
shift/reset using callcc/throw and a global meta-continuation.
