Using PVS to validate the algorithms of an exact arithmetic

Ko, 1983, On the definitions of some complexity classes of real numbers, Math. Systems Theory, 16, 95, 10.1007/BF01744572 V.A. Lee Jr., H.-J. Boehm, Optimizing programs over the constructive reals, in: Proc. ACM SIGPLAN’90 Conf. Programming Language Design and Implementation, 1990, pp. 102–111. V. Ménissier-Morain, Arithmétique exacte, Ph.D. Thesis, L'Université Paris VII, December 1994. Mostowski, 1957, On computable sequences, Fundamenta Mathematicae, 44, 37, 10.4064/fm-44-1-37-51 Müller, 1986, Subpolynomial complexity classes of real functions and real numbers, vol. 226, 284 N.T. Müller, Towards a real Real RAM: a prototype using C++, in: K.-I. Ko, N. Müller, K. Weihrauch (Eds.), Computability and Complexity in Analysis, Universität Trier, 1996, pp. 59–66, second CCA Workshop, Trier, August 22–23, 1996. N.T. Müller, Implementing limits in an interactive RealRAM, in: J.-M. Chesneaux, F. Jézéquel, J.-L. Lamotte, J. Vignes (Eds.), Third Real Numbers and Computers Conference, Université Pierre et Marie Curie, Paris 1998, pp. 59–66, Paris, France, April 27–29, 1998. Pour-El, 1989, 10.1007/978-3-662-21717-7 Rice, 1954, Recursive real numbers, Proc. Amer. Math. Soc., 5, 784, 10.1090/S0002-9939-1954-0063328-5 Robinson, 1951, Review of “Peter, R., Rekursive Funktionen”, J. Symbolic Logic, 16, 280 Specker, 1949, Nicht konstruktiv beweisbare Sätze der Analysis, J. Symbolic Logic, 14, 145, 10.2307/2267043 K. Weihrauch, Computability, EATCS Monographs on Theoretical Computer Science, vol. 9, Springer, Berlin, 1987.