## About

I am a long-standing contributor to the Isabelle proof assistant and former member of the theorem proving group at TUM. A particular focus of my work has been code generation from specifications in higher-order logic.

If you want to contact me with a question concerning Isabelle, it is
very likely that it should go to one of the Isabelle mailing lists. There you can find
a lot of helpful minds to support you – and an archive which will
help others in the future. For questions which do not fit in scope there,
you can reach me at `florian.haftmanninformatik.tu-muenchen.de`.

## Publications

- Florian Haftmann, Donald Kossmann, Alexander Kreutz: Efficient Regression Tests for Database Application Systems. CIDR 2005: 95-106.
- Florian Haftmann, Donald Kossmann, Eric Lo: Parallel Execution of Test Runs for Database Application Systems. VLDB 2005: 589-600.
- Florian Haftmann, Makarius Wenzel: Constructive Type Classes in Isabelle. BibTeX.
- Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews: Imperative Functional Programming with Isabelle/HOL. BibTeX.
- Klaus Aehlig, Florian Haftmann, Tobias Nipkow: A Compiled Implementation of Normalization by Evaluation. BibTeX.
- Stefan Berghofer, Lukas Bulwahn, Florian Haftmann: Turning inductive into equational specifications. BibTeX.
- Florian Haftmann, Makarius Wenzel: Local theory specifications in Isabelle/Isar. BibTeX.
- Florian Haftmann: Code
Generation from Specifications in Higher Order Logic. PhD thesis.
If you are eager to have a glimpse at it, consider the following guide. Both science and software engineering are dynamic business, and a work which resides at the intersection of both also is. So, parts of the work have been generalized and extended after submission, and superior descriptive resources have emerged since.

- Chapters 1 to 3
- This is the comprehensive reference for the meta theory of code generation in the context of Isabelle/HOL, providing a unified notational framework, with two exceptions as follows.
- Section 3.2.7 – dictionary construction
- See Code Generation via Higher-Order Rewrite Systems for a more general treatment.
- Section 3.4.2 – dictionaries in contravariant position
- The treatment of this problem has been generalized thanks to Lukas Bulwahn.
- Section 4.1 – datatype abstraction
- See Data Refinement in Isabelle/HOL for the state of the art.
- Section 4.2 to Section 4.5
- These sections form an overview on a selection of specific topics and examples, for each of which more specific references exist.
- Section 4.6 – applications of proof terms for code generation
- The issues dealt with here are not mentioned elsewhere in the literature so far.
- Chapter 5 – conclusion
- Some of the dreams mentioned here now have become reality.

- Florian Haftmann: From Higher-Order Logic to Haskell: There and Back Again. BibTeX.
- Florian Haftmann, Tobias Nipkow: Code Generation via Higher-Order Rewrite Systems. BibTeX.
- Klaus Aehlig, Florian Haftmann, Tobias Nipkow: A Compiled Implementation of Normalization by Evaluation. BibTeX.
- Florian Haftmann, Alexander Krauss, Ondřej Kunčar, Tobias Nipkow: Data Refinement in Isabelle/HOL. BibTeX.

## For Scintilla

- A ML highlighting mode for the Scintilla Text Editor, version 1.72 or higher.
- Also a Scala mode for Scintilla.
- Likewise, a Perl/Shell mode which does not suffer from silly syntax highlighting.