Type Classes and Overloading in Higher-Order Logic

Type classes and overloading are shown to be independent concepts that can both be added to simple higher-order logics in the tradition of Church and Gordon, without demanding more logical expressiveness. In particular, model-theoretic issues are not affected. Our metalogical results may serve as a foundation of systems like Isabelle/Pure that offer the user Haskell-style order-sorted polymorphism as an extended syntactic feature. The latter can be used to describe simple abstract theories with a single carrier type and a fixed signature of operations.

• Type: Conference
• Year: 1997
• Where: TPHOL
• Authors: Markus Wenzel
• Keywords: Automated Reasoning, Extended Syntactic Feature, Simple Abstract Theories, Single Carrier Type, TPHOL 1997