Skip Navigation


Journal of Logic and Computation Advance Access originally published online on August 2, 2008
Journal of Logic and Computation 2009 19(1):17-43; doi:10.1093/logcom/exn026
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (1)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bauer, A.
Right arrow Articles by Stone, C. A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2008. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

This article appears in the following Journal of Logic and Computation issue: Special Issue: Logic and Computation in the Real World: CiE 2007 [View the issue table of contents]

Original Articles

RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice

Andrej Bauer

Faculty of Mathematics and Physics, University of Ljubljana, Ljubljana, Slovenia
E-mail: Andrej.Bauer{at}fmf.uni-lj.si

Christopher A. Stone

Computer Science Department, Harvey Mudd College, Claremont, CA, USA
E-mail: stone{at}cs.hmc.edu

Received 29 September 2007.

Realizability theory is not just a fundamental tool in logic and computability. It also has direct application to the design and implementation of programs, since it can produce code interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.



References

  1. Barwise J. Admissible Sets and Structures. (1975) Berlin: Springer.
  2. Bauer A. The Realizability Approach to Computable Analysis and Topology. (2000) Pittsburgh, PA, USA: Carnegie Mellon University. PhD thesis.
  3. Bauer A, Kavkler I. Implementing real numbers with RZ. Fourth International Conference on Computability and Complexity in Analysis—Weihrauch K, Zhong N, eds. Electronic Notes in Theoretical Computer Science, 2007. Forthcoming.
  4. Bauer A, Stone CA. Specifications via realizability. (2006) Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering (CLASE 2005) in Edinburgh, Scotland, Vol. 153 of Electronic Notes in Theoretical Computer Science. 77–92.
  5. Bauer A, Stone CA. RZ: a tool for bringing constructive and computable mathematics closer to programming practice. In: Computation and Logic in the Real World, Third Conference on Computability in Europe, in Siena, Italy, Vol. 4497 of LNCS. (2007) Berlin: Springer. 28–42.
  6. Bauer A, Birkedal L, Scott DS. Equilogical spaces. In: Theoretical Computer Science. (2004) 1. Amsterdam: Elsevier. 35–59.
  7. Benl H, Berger U, Schwichtenberg H, Seisenberger M, Zuber W. Proof theory at work: program development in the Minlog system. In: Automated Deduction: A Basis for Applications. Volume II, Systems and Implementation Techniques.—Bibel W, Schmidt PH, eds. (1998) Dordrecht: Kluwer Academic Publishers.
  8. Bertot Y, Castéran P. Interactive Theorem Proving and Program Development. (2004) Berlin: Springer.
  9. Birkedal L. Developing Theories of Types and Computability. (1999) Pittsburgh, PA, USA: School of Computer Science, Carnegie Mellon University. PhD thesis.
  10. Bishop E, Bridges D. Constructive Analysis, Vol. 279 of Grundlehren der math. Wissenschaften. (1985) Berlin: Springer.
  11. Blanck J. Computability on Topological Spaces by Effective Domain Representations. (1997) Uppsala, Sweden: Uppsala University, Department of Mathematics.
  12. Blanck J. Domain representability of metric spaces. Annals of Pure and Applied Logic (1997) 83:225–247.[CrossRef][Web of Science]
  13. Blum L, Cucker F, Shub M, Smale S. Complexity and Real Computation. (1998) New York: Springer.
  14. Borodin A, Monro JI. The Computational Complexity of Algebraic and Numeric Problems. (1975) New York, London, Amsterdam: American Elsevier. Number 1 in Elsevier computer science library: Theory of computation series.
  15. Edalat A, Lieutier A. Domain theory and differential calculus (functions of one variable). Mathematical Structures in Computer Science (2004) 14:771–802.[CrossRef][Web of Science]
  16. Ershov YL, Goncharov SS, Nerode A, Remmel JB, eds. Handbook of Recursive Mathematics. (1998) Amsterdam: Elsevier.
  17. Escardó MH. PCFExtended with Real numbers. (1997) Edinburgh, Scotland, UK: Department of Computer Science, University of Edinburgh. PhD thesis.
  18. Harper R, Mitchell JC, Moggi E. Higher-order modules and the phase distinction. (1990) Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL’90) in San Francisco: ACM, Berlin. 341–354.
  19. Jacobs B. Categorical Logic and Type Theory. (1999) North-Holland, Amsterdam: Elsevier Science.
  20. Kahrs S, Sannella D, Tarlecki A. The definition of Extended ML: a gentle introduction. Theoretical Computer Science (1997) 173:445–484.[CrossRef][Web of Science]
  21. Kleene SC. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic (1945) 10:109–124.[CrossRef]
  22. Kleene SC, Vesley RE. The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. (1965) North-Holland, Amsterdam: North-Holland Publishing Company.
  23. Komagata Y, Schmidt DA. Implementation of intuitionistic type theory and realizability theory. In: Technical Report TR-CS-95-4. (1995) Manhattan, KS, USA: Kansas State University.
  24. Lambov B. RealLib: an efficient implementation of exact real arithmetic. Mathematical Structures in Computer Science (2007) 17:81–98.[CrossRef][Web of Science]
  25. Leroy X, Doligez D, Garrigue J, Rémy D, Vouillon J. The Objective Caml system, documentation and user's manual - release 3.08. In: Technical report. (2004) Rocquencourt, France: INRIA.
  26. Longley J. Matching typed and untyped realizability. Electronic Notes in Theoretical Computer Science (1999) 23:74–100.[CrossRef]
  27. Longley J. When is a functional program not a functional program? In: International Conference on Functional Programming (ICFP’99) in Paris. (1999) ACM. 1–7.
  28. Marcial-Romero JR, Escardó MH. Semantics of a sequential language for exact realnumber computation. (2004) Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS’04) in Turku, Finland: IEEE. 426–435.
  29. Müller N. The iRRAM: exact arithmetic in C++. In: Computability and Complexity in Analysis: 4th International Workshop, CCA 2000 Swansea, UK, September 17, 2000, Selected Papers, Number 2064 in Lecture Notes in Computer Science.—Blanck J, Brattka V, Hertling P, eds. (2001) Berlin: Springer. 222–252.
  30. Nordström B, Petersson K, Smith JM. Programming in Martin-Löf's Type Theory. (1990) USA: Oxford University Press.
  31. Post E. Recursive unsolvability of a problem of Thue. The Journal of Symbolic Logic (1947) 12:1–11.[CrossRef]
  32. Sannella D, Sokolowski S, Tarlecki A. Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Informatica (1992) 29:689–736.[CrossRef][Web of Science]
  33. Scott DS. Data types as lattices. SIAM Journal of Computing (1976) 5:522–587.[CrossRef]
  34. Troelstra AS, van Dalen D. Constructivism in Mathematics, An Introduction. (1988) 1. Amsterdam: North-Holland. Number 121 in Studies in Logic and the Foundations of Mathematics.
  35. Troelstra AS, van Dalen D. Constructivism in Mathematics, An Introduction. (1988) 2. North-Holland. Number 123 in Studies in Logic and the Foundations of Mathematics.
  36. Tucker JV, Zucker JI. Computable functions and semicomputable sets on many-sorted algebras. In: Handbook of Logic in Computer Science.—Abramsky S, Gabbay DM, Maibaum TSE, eds. (1998) 5. Oxford: Clarendon Press.
  37. Weihrauch K. Computable Analysis. (2000) Berlin: Springer.
  38. Yap CK. Theory of real computation according to EGC, 2006. Dagstuhl Seminar "Reliable Implementation of Real Number Algorithms: Theory and Practice", LNCS in 2006 in Dagstuhl, Germany, January 8–13 (2006).

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (1)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bauer, A.
Right arrow Articles by Stone, C. A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?