Context-based proofs of termination for typed delimited-control operators