Higher order quotients and their implementation in Isabelle HOL

  • Oscar Slotosch
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1275)


This paper describes the concept of higher order quotients and an implementation in Isabelle. Higher order quotients are a generalization of quotients. They use partial equivalence relations (PERs) instead of equivalence relations to group together different elements. This makes them applicable to arbitrary function spaces. Higher order quotients are conservatively implemented in the Isabelle logic HOL with a type constructor and a type class for PERs. Ordinary quotients are a special case of higher order quotients. An example shows how they can be used in Isabelle.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BH95]
    Michel Bidoit and Rolf Hennicker. Behavioural Theories and The Proof of Behavioural Properties. Technical report, Paris, 1995.Google Scholar
  2. [BM92]
    Kim Bruce and and John C. Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In Principles of Programming Languages 19, pages 316–327, Albequerque, New Mexico, 1992. Albequerque, New Mexico, 1992.Google Scholar
  3. [Chu40]
    Alonzo Church. A formulation of the simple theory of types. J. Symbolic Logic, 5:56–68, 1940.Google Scholar
  4. [GM93]
    M. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.Google Scholar
  5. [Har96]
    John Robert Harrison. Theorem Proving with the Real Numbers. PhD thesis, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1996. Technical Report No 408.Google Scholar
  6. [HJW92]
    P. Hudak, S. Peyton Jones, and P. Wadler, editors. Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.2). ACM SIGPLAN Notices, May 1992.Google Scholar
  7. [Jon93]
    M. P. Jones. An Introduction to Gofer, August 1993.Google Scholar
  8. [Nip91]
    T. Nipkow. Order-Sorted Polymorphism in Isabelle. In G. Huet, G. Plotkin, and C. Jones, editors, Proc. 2nd Workshop on Logical Frameworks, pages 307–321, 1991.Google Scholar
  9. [Pau94]
    Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994.Google Scholar
  10. [Reg94]
    Franz Regensburger. HOLCF: Eine konservative Erweiterung von HOL um LCF. PhD thesis, Technische Universität München, 1994.Google Scholar
  11. [Rob89]
    Edmund Robinson. How Complete is PER? In Fourth Annual Symposium on Logic in Computer Science, pages 106–111, 1989.Google Scholar
  12. [Slo97]
    Oscar Slotosch. Refinements in HOLCF: Implementation of Interactive Systems. PhD thesis, Technische Universität München, 1997.Google Scholar
  13. [Völ95]
    Norbert Völker. On the Representation of Datatypes in Isabelle/HOL. Technical Report 379, University of Cambridge Computer Laboratory, 1995. Proceedings of the First Isabelle Users Workshop.Google Scholar
  14. [Wen94]
    Markus Wenzel. Axiomatische Typklassen in Isabelle. Master's thesis, Institut für Informatik, TU München, 1994.Google Scholar
  15. [Wen95]
    M. Wenzel. Using axiomatic type classes in Isabelle — a tutorial, 1995. Available at Scholar
  16. [Wen97]
    M. Wenzel. Type Classes and Overloading in Higher-Order Logic. In Proceedings of Theorem Proving in Higher Order Logics, 1997. in this volume.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Oscar Slotosch
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations