Skip to main content
SpringerLink
Log in

A Principle of Induction

  • Conference paper
  • First Online:
Computer Science Logic (CSL 2001)

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

Included in the following conference series:

Abstract

We introduce an induction principle on complete partial orders and consider its applications to program verification and analysis on the real line. The highlight of this technique is that it allows one to make inductive arguments over continuous as well as discrete forms of data without ever having to distinguish between the two.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. S. Abramsky and A. Jung, Domain theory. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994.

    Google Scholar 

  2. P. Aczel, An introduction to inductive definitions. In Handbook of Mathematical Logic, J. Barwise, Editor, North-Holland, p. 739–782.

    Google Scholar 

  3. T. Coquand, Constructive topology and combinatorics. Lecture Notes in Computer Science, vol. 613, p. 159–164.

    Book  Google Scholar 

  4. T. Coquand, A note on the open induction principle. http://www.cs.chalmers.se/ coquand/open.ps.Z

  5. M. Escardo and T. Streicher, Induction and recursion on the partial real line with applications to Real PCF. Theoretical Computer Science, volume 210, number 1, p. 121–157, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  6. K. Martin, A foundation for computation. Ph.D. Thesis, Department of Mathematics, Tulane University, May 2000. http://web.comlab.ox.ac.uk/oucl/work/keye.mart in

  7. K. Martin, The measurement process in domain theory. Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, vol. 1853, Springer-Verlag, 2000.

    Chapter  Google Scholar 

  8. L.C. Paulson, ML for the Working Programmer. Cambridge University Press, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD

    Keye Martin

Authors
  1. Keye Martin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LSV (Ecole Normale Supérieure de Cachan and CNRS), 61, Avenue du Président Wilson, 94230, Cachan, France

    Laurent Fribourg

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Martin, K. (2001). A Principle of Induction. In: Fribourg, L. (eds) Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44802-0_32

Download citation

  • DOI: https://doi.org/10.1007/3-540-44802-0_32

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42554-0

  • Online ISBN: 978-3-540-44802-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation