Certifying Dictionary Construction in Isabelle/HOL

Type classes are a well-known extension to various type systems. Classes usually participate in type inference; that is, the type checker will automatically deduce class constraints and select appropriate instances. Compilers for such languages face the challenge that concrete instances are generally not directly mentioned in the source text. In the runtime, type class operations need to be packaged into dictionaries that are passed around as pointers. This article presents the most common approach for compilation of type classes - the dictionary construction - carried out in a trustworthy fashion in Isabelle/HOL, a proof assistant. The result is an automatic routine that eliminates occurences of classes and instances from a set of definitions and proves a theorem relating old and new definitions.