Advertisement!: Paulo de Vilhena’s PhD dissertation, whose main theme is formal reasoning about programs that involve effect handlers, contains chapters about the connections between callcc/throw, shift/reset, and effect handlers (including encodings between these combinators and proofs that these encodings give rise to the expected reasoning rules).
It also contains a specification and a proof of correctness for invert, a function that uses effect handlers to turn an iter function into a lazy sequence.