  We derive a Hoare-Floyd logic for non-local jumps and mutable higher-order
procedural variables from a formul{\ae}-as-types notion of control for
classical logic. The main contribution of this work is the design of an
imperative dependent type system for non-local jumps which corresponds to
classical logic but where the famous consequence rule is still derivable.
