[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Constructive Type Classes in Isabelle

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

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

Included in the following conference series:

Abstract

We reconsider the well-known concept of Haskell-style type classes within the logical framework of Isabelle. So far, axiomatic type classes in Isabelle merely account for the logical aspect as predicates over types, while the operational part is only a convention based on raw overloading. Our more elaborate approach to constructive type classes provides a seamless integration with Isabelle locales, which are able to manage both operations and logical properties uniformly. Thus we combine the convenience of type classes and the flexibility of locales. Furthermore, we construct dictionary terms derived from notions of the type system. This additional internal structure provides satisfactory foundations of type classes, and supports further applications, such as code generation and export of theories and theorems to environments without type classes.

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

Access this chapter

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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.

Similar content being viewed by others

References

  1. Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, Springer, Heidelberg (2004)

    Google Scholar 

  2. Ballarin, C.: Interpretation of locales in Isabelle: Theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Chrzaszcz, J.: Modules in type theory with generative definitions. PhD thesis, Université Paris-Sud (2004)

    Google Scholar 

  5. Courant, J.: \(\mathcal{MC}_2\): A Module Calculus for Pure Type Systems. The Journal of Functional Programming (to appear, 2006)

    Google Scholar 

  6. Hall, C., Hammond, K., Peyton Jones, S., Wadler, P.: Type classes in Haskell. ACM Transactions on Programming Languages and Systems 18(2) (1996)

    Google Scholar 

  7. Jones, S., Jones, M., Meijer, E.: Type classes: an exploration of the design space (1997)

    Google Scholar 

  8. Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Nipkow, T.: Order-sorted polymorphism in Isabelle. In: Huet, G., Plotkin, G. (eds.) Logical Environments, Cambridge University Press, Cambridge (1993)

    Google Scholar 

  11. Nipkow, T.: Structured proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. In: Nipkow, T., Paulson, L.C., Wenzel, M. (eds.) Isabelle/HOL. LNCS, vol. 2283, Springer, Heidelberg (2002)

    Google Scholar 

  13. Nipkow, T., Prehofer, C.: Type checking type classes. In: ACM Symp. Principles of Programming Languages, ACM Press, New York (1993)

    Google Scholar 

  14. Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, Academic Press, London (1990)

    Google Scholar 

  15. Peterson, J., Jones, M.P.: Implementing type classes. In: SIGPLAN. Conference on Programming Language Design and Implementation (1993)

    Google Scholar 

  16. Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  17. Schmidt-Schauß, M.: Computational Aspects of an Order-Sorted Logic with Term Declarations. LNCS, vol. 395. Springer, Heidelberg (1989)

    MATH  Google Scholar 

  18. Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad-hoc. In: ACM Symp. Principles of Programming Languages, ACM Press, New York (1989)

    Google Scholar 

  19. Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  20. Wenzel, M.: Isar — a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Wenzel, M.: Isabelle/Isar — a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, TU München (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Thorsten Altenkirch Conor McBride

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Haftmann, F., Wenzel, M. (2007). Constructive Type Classes in Isabelle. In: Altenkirch, T., McBride, C. (eds) Types for Proofs and Programs. TYPES 2006. Lecture Notes in Computer Science, vol 4502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74464-1_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74464-1_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74463-4

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics