Skip to main content
SpringerLink
Log in

QArith: Coq Formalisation of Lazy Rational Arithmetic

  • Conference paper
Types for Proofs and Programs (TYPES 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3085))

Included in the following conference series:

Abstract

In this paper we present the Coq formalisation of the QArith library which is an implementation of rational numbers as binary sequences for both lazy and strict computation. We use the representation also known as the Stern-Brocot representation for rational numbers. This formalisation uses advanced machinery of the Coq theorem prover and applies recent developments in formalising general recursive functions. This formalisation highlights the rôle of type theory both as a tool to verify hand-written programs and as a tool to generate verified programs.

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. Balaa, A., Bertot, Y.: Fonctions récursives générales par itération en théorie des types. In: Proceedings of JFLA 2002. INRIA (2002)

    Google Scholar 

  2. Barthe, G., Courtieu, P.: Efficient Reasoning about Executable Specifications in Coq. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 31–46. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Bertot, Y.: Simple canonical representation of rational numbers. In: Geuvers, H., Kamareddine, F. (eds.) Electronic Notes in Theoretical Computer Science, vol. 85(7), Elsevier, Amsterdam (2003)

    Google Scholar 

  4. Bertot, Y., Castéran, P.: Coq’Art. To be published by Springer, Heidelberg (2004)

    MATH  Google Scholar 

  5. Bove, A., Capretta, V.: Nested general recursion and partiality in type theory. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 121–135. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 4. INRIA (February 2003), http://coq.inria.fr/doc/main.html

  7. Delahaye, D., Mayero, M.: Field: une procédure de décision pour les nombres réels en Coq. In: Proceedings of JFLA 2001. INRIA (2001)

    Google Scholar 

  8. Gosper, R.W.: HAKMEM, Item 101 B. MIT AI Laboratory Memo No.239 (February 1972), http://www.inwap.com/pdp10/hbaker/hakmem/cf.html#item101b

  9. Konečný, M.: Many-Valued Real Functions Computable by Finite Transducers using IFS-Representations. PhD thesis, The University of Birmingham (October 2000)

    Google Scholar 

  10. Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 388–405. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Magaud, N.: Changing Data Representation within the Coq System. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 87–102. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Ménissier-Morain, V.: Arithmétique exacte, conception, algorithmique et performances d’une implémentation informatique en précision arbitraire. Thèse, Universit é Paris 7 (December 1994)

    Google Scholar 

  13. Niqui, M.: Exact Arithmetic on Stern–Brocot Tree. Technical Report NIII-R0325, Nijmegen Institute for Computer and Information Sciences (November 2003)

    Google Scholar 

  14. Niqui, M., Bertot, Y.: Coq contribution (May 2003), http://coqcvs.inria.fr/cgi-bin/cvswebcoq.cgi/contrib/Nijmegen/QArith/

  15. Paulin, C.: Coq club mailing list correspondence (August 2002)

    Google Scholar 

  16. Paulin-Mohring, C.: Extracting Fω’s programs from proofs in the Calculus of Constructions. In: Proceedings of POPL 1989, January 1989, pp. 89–104. ACM, New York (1989)

    Google Scholar 

  17. Potts, P.J.: Exact Real Arithmetic using Möbius Transformations. PhD thesis, University of London, Imperial College (July 1998)

    Google Scholar 

  18. Vuillemin, J.E.: Exact real computer arithmetic with continued fractions. IEEE Transactions on Computers 39(8), 1087–1105 (1990)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Nijmegen,  

    Milad Niqui

  2. INRIA Sophia Antipolis,  

    Yves Bertot

Authors
  1. Milad Niqui
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yves Bertot
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Stefano Berardi

  2. Dipartimento di Informatica, Università di Torino,  

    Mario Coppo

  3. Dipartimento di Informatica, Università di Torino, Corso Svizzera, 185, I-10149, Torino, Italy

    Ferruccio Damiani

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Niqui, M., Bertot, Y. (2004). QArith: Coq Formalisation of Lazy Rational Arithmetic. In: Berardi, S., Coppo, M., Damiani, F. (eds) Types for Proofs and Programs. TYPES 2003. Lecture Notes in Computer Science, vol 3085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24849-1_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24849-1_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22164-7

  • Online ISBN: 978-3-540-24849-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation