Code generation denotes the translation of an abstract formal specification into a corresponding executable program. The aim of this thesis is to present a code generator framework for the interactive proof assistant Isabelle/HOL, an implementation of higher-order logic. It comes with two substantial novelties: a general but lightweight concept for datatype abstraction and support for Isabelle type classes in the manner of Haskell type classes. Code can be generated for functional programming languages supporting pattern matching; concrete instances for SML, OCaml and Haskell are presented.

PhD thesis.