Skip to main content
SpringerLink
Log in

Proofs, Programs, Processes

  • Conference paper
Programs, Proofs, Processes (CiE 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6158))

Included in the following conference series:

Abstract

We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers w.r.t. to the binary signed digit representation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.H. (eds.) Automated Deduction – A Basis for Applications. Applied Logic Series, vol. II, pp. 41–71. Kluwer, Dordrecht (1998)

    Google Scholar 

  2. Berger, U.: From coinductive proofs to exact real arithmetic. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 132–146. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Berger, U.: Realisability and adequacy for (co)induction. In: Bauer, A., Hertling, P., Ko, K.-I. (eds.) 6th Int’l Conf. on Computability and Complexity in Analysis (Ljubljana), Dagstuhl, Germany. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2009)

    Google Scholar 

  4. Berger, U., Hou, T.: Coinduction for exact real number computation. Theory of Computing Systems 43, 394–409 (2008)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  7. 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.) Applied Semantics - Lecture Notes from the International Summer School, Caminha, Portugal, pp. 193–267. Springer, Heidelberg (2002)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  10. Hernest, M.D., Oliva, P.: Hybrid functional interpretations. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 251–260. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  12. The Minlog System, http://www.mathematik.uni-muenchen.de/~minlog/

  13. Miranda-Perea, F.: Realizability for monotone clausular (co)inductive definitions. Electr. Notes in Theoret. Comput. Sci. 123, 179–193 (2005)

    Article  MathSciNet  Google Scholar 

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

    MathSciNet  Google Scholar 

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

    Google Scholar 

  16. Ratiu, D., Trifonov, T.: Exploring the computational content of the infinite pigeonhole principle. Journal of Logic and Computation (to appear 2010)

    Google Scholar 

  17. Schwichtenberg, H.: Realizability interpretation of proofs in constructive analysis. Theory of Computing Systems 43(3-4), 583–602 (2008)

    Article  MATH  MathSciNet  Google Scholar 

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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Swansea University, Swansea, SA2 8PP, Wales, UK

    Ulrich Berger & Monika Seisenberger

Authors
  1. Ulrich Berger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Monika Seisenberger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Matemática, Universidade de Lisboa, Campo Grande, Edifício C6, 1749-016, Lisboa, Portugal

    Fernando Ferreira

  2. Institute for Logic, Language and Computation (ILLC), Universiteit van Amsterdam, P.O. Box 94242, 1090, Amsterdam, GE, The Netherlands

    Benedikt Löwe

  3. Departamento de Informática e Ingeniería de Sistemas, Universidad de Zaragoza, María de Luna 1, 50018, Zaragoza, Spain

    Elvira Mayordomo

  4. Universidade dos Açores, Campus de Ponta Delgada, Apartado 1422, 9501-801, Ponta Delgada, Açores, Portugal

    Luís Mendes Gomes

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Berger, U., Seisenberger, M. (2010). Proofs, Programs, Processes. In: Ferreira, F., Löwe, B., Mayordomo, E., Mendes Gomes, L. (eds) Programs, Proofs, Processes. CiE 2010. Lecture Notes in Computer Science, vol 6158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13962-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13962-8_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13961-1

  • Online ISBN: 978-3-642-13962-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation