Shouldn't this script terminate on ^C?

[Nikolaus Schulz]

Please consider this bash script:

  : | while true; do sleep 1; done
  echo "After loop"

If I hit ^C while it runs, shouln't it terminate?

I have tested bash versions 4.2.37(1)-release, 4.1.5(1)-release,
and 3.2.39(1)-release. (Debian Sid, Squeeze and Lenny.)

All these bash versions output "After loop".
zsh and dash do exit immediately.  Which behaviour is correct?
I couldn't find what POSIX says about this.

Thank you,
Nikolaus