\lettrine[nindent=0ex]I{} have to thank Prof.\@ Gregor Snelting for giving me the possibility to join his group and to work on this thesis. He expected and allowed me to work with great freedom and latitude, and I could pursue my own ideas without pressure or worries.

I also thank Prof.\@ Tobias Nipkow for serving as the co-referee, but also for creating Isabelle in the first place. Without his work, two thirds of this thesis would not exist.

I am indebted to Simon Peyton Jones, with whom I spent three months as an intern. This was a very fruitful time that heavily influenced my work. He pointed me to the open problem of making \hi{foldl} a good consumer, which initiated the whole work on Call Arity, and nudged me to go further when I thought my solution was “good enough”. Furthermore, I enjoyed the privilege to be his co-author. Finally, without his work on GHC and Haskell, two thirds of this thesis would not exist.

\medskip

I was able to pursue my research with few constraints, and was able to attend summer schools and conferences, due to a generous scholarship by the Deutsche Telekom Stiftung. I thank Prof.\@ Sigmar Wittig for his commitment as a mentor and for keeping me on track in critical times, and Christiane Frense-Heck for managing the scholarship program so very efficiently, smoothly and friendly. I also thank Gabriela Weitze-Schmithüsen for helping me to secure the scholarship in the first place, and for not holding a grudge after I left her research group.

\medskip

The programming paradigms group at the Karlsruhe Institute of Technology has been a great place to work at, and I am happy that I was part of this group. In particular I would like to thank my colleagues for 3-pm-rituals, board game nights and a roughly monthly supply of cake. Special thanks go to my office mate Denis Lohner, who was always available to discuss questions with, and my former office mate Andreas Lochbihler, who initiated me to semantics and interactive theorem proving.

I thank Martin Mohr, Sebastian Buchwald, Denis Lohner, Manuel Mohr, Mareike Schmidtobreick, Ulrike Leyn and Thomas Breitner for proofreading a draft of this thesis.

\medskip

Finally, I’d like to thank Isabelle for a great many hours of working together in solitude. She is sometimes difficult to work with, but her endless patience and unerring pedantry taught me a lot. She would not take a \isa{sorry}, but when I admitted that she is -- as always -- right and I made up for my mistakes, she never was resentful.

I also thank the other Isabelle for being so quite different: always available for a little quiz, other games or just a mindless chat.