  Recently, the second author, Briseid and Safarik introduced nonstandard
Dialectica, a functional interpretation that is capable of eliminating
instances of familiar principles of nonstandard arithmetic - including
overspill, underspill, and generalisations to higher types - from proofs. We
show that, under few metatheoretical assumptions, the properties of this
interpretation are mirrored by first order logic in a constructive sheaf model
of nonstandard arithmetic due to Moerdijk, later developed by Palmgren. In
doing so, we also draw some new connections between nonstandard principles, and
principles that are rejected by strict constructivism.
  Furthermore, we introduce a variant of the Diller-Nahm interpretion with two
different kinds of quantifiers (with and without computational meaning),
similar to Hernest's light Dialectica interpretation, and show that one can
obtain nonstandard Dialectica from this by weakening the computational content
of the existential quantifiers -- a process we call herbrandisation. We also
define a constructive sheaf model mirroring this new functional interpretation
and show that the process of herbrandisation has a clear meaning in terms of
these sheaf models.
