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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Haftmann, F., & Wenzel, M. (2007). Constructive type classes in isabelle. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4502 LNCS, pp. 160–174). Springer Verlag. https://doi.org/10.1007/978-3-540-74464-1_11
Mendeley helps you to discover research relevant for your work.