One application I know is Scott's construction of forcing extensions of models of higher order theories of the Real numbers. Scott quickly after the invention of forcing, used a forcing argument to show that the Continuum Hypothesis is independent of an axiomatization of Second Order Analysis.
He interpreted first order variables (usually real numbers) as Random Variables over a complete Boolean Algebra with the ccc, second order variables (usually functions from the reals to the reals) as functions from RV to RV, satisfying a certain technical condition and then defined the Boolean value of each statement, which is an element of the Boolean algebra. He then showed that the axioms have Boolean Value $\mathbb{1}$ and that the inference rules respect the Boolean value (i.e. do not decrease the Boolean value) and finally exhibits a Boolean algebra in which the statement $CH$ has Boolean value $\ne \mathbb{1}$. See here for more details:
http://link.springer.com/content/pdf/10.1007%2FBF01705520.pdf
All in all this line of argumentation preshadows the way (set theoretic) forcing is presented in (for example) Jech's book, which explains forcing as forcing with Boolean valued models of the universe $V$.
The question is extremely interesting, and I have looked into this kind of thing with various colleagues (including Russell Miller and Kameryn Williams), although our investigation has not yet resulted in any paper.
One important realization to which we had come was that the question is highly sensitive to whether the input data includes just the set-membership information, or instead the diagram (the truths) of the original model.
With an oracle for the elementary diagram of a countable model $\langle M,\in^M\rangle$ of a model of set theory, that is, an oracle listing all the true statements of the model, with names for every element, then for any forcing notion $\mathbb{P}$ in $M$, one can compute an $M$-generic filter $G$ and the elementary diagram of the corresponding forcing extension $M[G]$. This can be seen as a strong positive answer to your question. The reason you can find such a $G$ is that the oracle for the diagram of $M$ allows you to find a canonical enumeration of the dense sets of $M$, and so by the usual diagonalization, one can compute a filter getting into all those dense sets, and this filter will therefore be generic. (In this sense, your remarks about multi-valued seem to be unnecessary — one can compute a specific generic filter.) Using this filter $G$, one can evaluate the diagram of the extension $V[G]$ in terms of names, using the forcing relation, which is expressed in the diagram of the original model. Thus, from the diagram of a model $M$, you can compute the diagram of the forcing extension $M[G]$.
In particular, this shows that from the diagram of any model of ZFC, you can compute the diagram of a model of ZFC+CH or of ZFC+$\neg$CH or ZFC+MA and so on, for all the various results obtained by forcing.
One can also compute the elementary diagram of many other kinds of set-theoretic constructions, such as inner models $L$ and $\text{HOD}$, and ultrapowers $\text{Ult}(M,\mu)$ by an ultrafilter $\mu$ in $M$, or an extender ultrapower.
You don't need the whole diagram to compute the generic filter $G$, and in fact, even just the atomic diagram, which contains information only about the membership relation $n\in m$ for specific objects, is sufficient to compute a generic filter $G$. One simply fixes the object whose elements are the dense subsets of $\mathbb{P}$ and an object for the order relation, and then you can carry out the diagonalization.
Nevertheless, and this is an important point, if all you have is the atomic diagram of the original model $M$, then it turns out that you cannot compute much about the model or its forcing extensions at all. For example, you cannot even reliably identify from the atomic diagram which is the empty set of $M$, since for any computable algorithm, there is a model $M$ that will fool it. And there are many further such examples. I take these examples to illustrate that one shouldn't think of a model of set theory merely as its atomic diagram, but as a bit more.
Best Answer
It seems that Lars Brünjes and Christian Serpé have a whole program for introducing non standard mathematics in algebraic geometry; they wish to play with non standard contructions, seen internally and externally (the interest of this game consists precisely to look at the non-classical logic (or internal) point of view and at the classical (or external) one at the same time). For instance, for an infinite prime number $P$, the ring $\mathbf{Z}/P\mathbf{Z}$ behaves internally like a finite field, while externally, it is a field of characteristic zero which contains an algebraic closure of $\mathbf{Q}$. Non-standard constructions can often be interpreted in a precise way as standard ones using ultraproducts and ultrafilters. Their purpose is to develop all the tools of classical algebraic geometry (homotopical and homological algebra, stacks, étale cohomology, algebraic K-theory, higher Chow groups...) in a non-standard way, in order to prove facts in the classical setting. Most of their papers can be found here (their papers contains more precise ideas on the possible interpretations and explanations). Brünjes and Serpé see non-standard mathematics as an enlargement of standard mathematics, and their work deals a lot in making this precise. However, they seem to have quite few concrete problems in mind. For instance, they have found sufficient conditions on cohomology classes to be algebraic in a very classical sense (see arXiv:0901.4853).