From Coinductive Proofs to Exact Real Arithmetic

1. Marcial-Romero, J.R., Escardo, M.H.: Semantics of a sequential language for exact real-number computation. Theor. Comput. Sci. 379, 120–141 (2007)

   MathSciNet  MATH  Google Scholar 

2. Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17, 3–36 (2007)

   Article  MathSciNet  MATH  Google Scholar 

3. Edalat, A., Heckmann, R.: Computing with real numbers: I. The LFT approach to real number computation; II. A domain framework for computational geometry. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 193–267. Springer, Heidelberg (2002)

   Chapter  Google Scholar 

4. Ciaffaglione, A., Di Gianantonio, P.: A certified, corecursive implementation of exact real numbers. Theor. Comput. Sci. 351, 39–51 (2006)

   MathSciNet  MATH  Google Scholar 

5. Bertot, Y.: Affine functions and series with co-inductive real numbers. Math. Struct. Comput. Sci. 17, 37–63 (2007)

   Article  MathSciNet  MATH  Google Scholar 

6. Berger, U., Hou, T.: Coinduction for exact real number computation. Theory Comput. Sys. (to appear, 2009)

   Google Scholar 

7. Niqui, M.: Coinductive formal reasoning in exact real arithmetic. Logical Methods in Computer Science 4, 1–40 (2008)

   Article  MathSciNet  MATH  Google Scholar 

8. Schwichtenberg, H.: Realizability interpretation of proofs in constructive analysis. Theory Comput. Sys. (to appear, 2009)

   Google Scholar 

9. Berger, U., Seisenberger, M.: Applications of inductive definitions and choice principles to program synthesis. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis Towards practicable foundations for constructive mathematics. Oxford Logic Guides, vol. 48, pp. 137–148. Oxford University Press, Oxford (2005)

   Chapter  Google Scholar 

10. Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electr. Notes in Theoret. Comp. Sci. 164 (2006)

    Google Scholar 

11. Buchholz, W., Feferman, F., Pohlers, W., Sieg, W.: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof–Theoretical Studies. Lecture Notes in Mathematics, vol. 897. Springer, Berlin (1981)

    Book  MATH  Google Scholar 

12. Bradfield, J., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3, pp. 721–756. Elsevier, Amsterdam (2007)

    Chapter  Google Scholar 

13. Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: Continuous Lattices and Domains. Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge University Press, Cambridge (2003)

    Book  MATH  Google Scholar 

14. Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics, 101–128 (1959)

    Google Scholar 

15. Tatsuta, M.: Realizability of monotone coinductive definitions and its application to program synthesis. In: Jeuring, J. (ed.) MPC 1998. Lecture Notes in Mathematics, vol. 1422, pp. 338–364. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

16. Troelstra, A.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Heidelberg (1973)

    MATH  Google Scholar 

17. Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handb. Logic Comput. Sci., vol. 3, pp. 1–168. Clarendon Press, Oxford (1994)

    Google Scholar 

18. Malcolm, G.: Data structures and program transformation. Science of Computer Programming 14, 255–279 (1990)

    Article  MathSciNet  MATH  Google Scholar 

19. Hancock, P., Setzer, A.: Guarded induction and weakly final coalgebras in dependent type theory. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, pp. 115–134. Clarendon Press, Oxford (2005)

    Chapter  Google Scholar 

20. Abel, A., Matthes, R., Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333, 3–66 (2005)

    MathSciNet  MATH  Google Scholar 

21. Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Information and Computation 204, 437–468 (2006)

    Article  MathSciNet  MATH  Google Scholar 

22. Konečný, M.: Real functions incrementally computable by finite automata. Theor. Comput. Sci. 315, 109–133 (2004)

    MathSciNet  MATH  Google Scholar 

23. Blanck, J.: Efficient exact computation of iterated maps. Journal of Logic and Algebraic Programming 64, 41–59 (2005)

    Article  MathSciNet  MATH  Google Scholar 

24. Plume, D.: A Calculator for Exact Real Number Computation. PhD thesis. University of Edinburgh (1998)

    Google Scholar 

25. Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., Zuber, W.: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction – A Basis for Applications. Applied Logic Series, vol. II, pp. 41–71. Kluwer, Dordrecht (1998)

    Chapter  Google Scholar 

26. Scriven, A.: A functional algorithm for exact real integration with invariant measures. Electron. Notes Theor. Comput. Sci. 218, 337–353 (2008)

    Article  MATH  Google Scholar 

Download references