Skip to main content
SpringerLink
Log in

HOL Constant Definition Done Right

  • Conference paper
Interactive Theorem Proving (ITP 2014)

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

Included in the following conference series:

Abstract

This note gives a proposal for a simpler and more powerful replacement for the mechanisms currently provided in the various HOL implementations for defining new constants.

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. Adams, M.: HOL Zero, http://www.proof-technologies.com/holzero/

  2. Arthan, R., Jones, R.B.: Z in HOL in ProofPower. BCS FACS FACTS (2005-1), http://www.lemma-one.com/ProofPower/index/

  3. Harrison, J.: HOL light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009), http://www.cl.cam.ac.uk/~jrh13/hol-light/

    Chapter  Google Scholar 

  4. Homeier, P.V.: The HOL-Omega logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 244–259. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: HOL with definitions: Semantics, soundness, and a verified implementation. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS (LNAI), vol. 8558, pp. 308–324. Springer, Heidelberg (2014)

    Google Scholar 

  6. Wenzel, M., et al.: The Isabelle/Isar Reference Manual, http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf

  7. Norrish, M., et al.: The HOL System: Logic, 3rd edn., http://hol.sourceforge.net/documentation.html

  8. Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Lemma 1 Ltd./ School of Electronic Engineering and Computer Science, Queen Mary, University of London, UK

    Rob Arthan

Authors
  1. Rob Arthan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NICTA, Sydney, NSW, Australia

    Gerwin Klein

  2. University of Wyoming, Laramie, WY, USA

    Ruben Gamboa

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Arthan, R. (2014). HOL Constant Definition Done Right. In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08970-6_34

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08969-0

  • Online ISBN: 978-3-319-08970-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation