Dear Paul and Andrej, I was aware of the fact that locatedness is part of definition of Dedekind cut it guarantees. It guarantees that there are close enough approximations for any required degree of precision. Having had a look at Andrej's slides I can't say that they provided me with an understanding of the operational semantics of the language. The impression I got is that he is using (kind of) interval arithmetic for determining truth values of terms of type \Sigma. That's ok but doesn't answer the question what is a computationally given real number. Do I understand your approach correctly as follows: when given a Dedekind cut as a mapping c : Q -> 2_\bot and an accuracy eps then \exists p,q : Q c(p) = 0 /\ c(q) = 1 /\ q-p < eps is true and computing this truth value gives the witnesses p and q. I.e. one evaluates terms of type \Sigma of the ASD language in a way reminiscent of logic programming. Thomas