Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 2005: Theorem Proving in Higher Order Logics pp 147–162Cite as

Axiomatic Constructor Classes in Isabelle/HOLCF

  • Conference paper

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

Abstract

We have definitionally extended Isabelle/HOLCF to support axiomatic Haskell-style constructor classes. We have subsequently defined the functor and monad classes, together with their laws, and implemented state and resumption monad transformers as generic constructor class instances. This is a step towards our goal of giving modular denotational semantics for concurrent lazy functional programming languages, such as GHC Haskell.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Clarendon Press (1994)

    Google Scholar 

  2. Roberto, M.: Domains and Lambda Calculi. Cambridge Tracts in Theoretical Computer Science, vol. 46. Cambridge University Press, Cambridge (1998)

    MATH  Google Scholar 

  3. Ballarin, C.: Locales and locale expressions in isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCs, vol. 3085, pp. 34–50. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Bertot, Y., Castéran, P.: Interactive theorem proving and program development. In: Coq’Art: The calculus of inductive constructions. Texts in Theoretical Computer Science, p. 492 (2004)

    Google Scholar 

  5. Farmer, W.M.: An infrastructure for intertheory reasoning. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 115–131. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. Farmer, W.M., Guttman, J.D., Thayer Fábrega, F.J.: IMPS: An updated system description. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 298–302. Springer, Heidelberg (1996)

    Google Scholar 

  7. Gunter, C.A., Scott, D.S.: Semantic domains. In: Handbook of theoretical computer science formal models and semantics, vol. B, pp. 633–674. MIT Press, Cambridge (1990)

    Google Scholar 

  8. Hickey, J., Nogin, A., Constable, R.L., Aydemir, B.E., Barzilay, E., Bryukhov, Y., Eaton, R., Granicz, A., Kopylov, A., Kreitz, C., Krupski, V.N., Lorigo, L., Schmitt, S., Witty, C., Yu, X.: MetaPRL—A modular logical environment, pp. 287–303

    Google Scholar 

  9. Johnsen, E.B., Lüth, C.: Theorem reuse by proof term transformation. In: Slind, K., Bunker, A., Gopalakrishnan, G.(eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 152–167. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Jones, M.P.: Programatica web page (2005), http://www.cse.ogi.edu/PacSoft/projects/programatica

  11. Jones, S.P.: Haskell98 Language and Libraries, Revised Report (December 2002)

    Google Scholar 

  12. 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, p. 149. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Melham, T.F.: The HOL logic extended with quantification over type variables. In: HOL 1992: Proceedings of the IFIP TC10/WG10.2 Workshop on Higher Order Logic Theorem Proving and its Applications, pp. 3–17. North-Holland/Elsevier, Amsterdam (1993)

    Google Scholar 

  14. Müller, O., Nipkow, T., Von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9(2), 191–223 (1999)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    MATH  Google Scholar 

  17. Owre, S., Shankar, N.: Theory interpretations in PVS. Technical Report SRI-CSL-01-01, Computer Science Laboratory, SRI International, Menlo Park, CA (April 2001)

    Google Scholar 

  18. Papaspyrou, N.S.: A formal semantics for the C programming language. PhD thesis, National Technical University of Athens, Department of Electrical and Computer Engineering, Software Engineering Laboratory (February 1998)

    Google Scholar 

  19. Papaspyrou, N.S., Macos, D.: A study of evaluation order semantics in expressions with side effects. Journal of Functional Programming 10(3), 227–244 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  20. Regensburger, F.: HOLCF: Higher order logic of computable functions. In: Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, pp. 293–307. Springer, Heidelberg (1995)

    Google Scholar 

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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. OGI School of Science and Engineering at OHSU, Beaverton, OR, 97006

    Brian Huffman, John Matthews & Peter White

Authors
  1. Brian Huffman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Matthews
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter White
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, Oxford University,  

    Joe Hurd

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

    Tom Melham

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huffman, B., Matthews, J., White, P. (2005). Axiomatic Constructor Classes in Isabelle/HOLCF. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_10

Download citation

  • DOI: https://doi.org/10.1007/11541868_10

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation