About
I am a long-standing contributor to the Isabelle proof assistant and former member of the theorem proving group at TUM. My contributions covered the following topics:
- Code generation from specifications in higher-order logic.
- Computational abstract algebra.
- Isabelle's module system: locales, locale interpretation, type classes and local theories.
- Wide-spread maintenance work on Isabelle/HOL library theories.
See further CONTRIBUTORS.
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.haftmann
informatik.tu-muenchen.de.
Publications
- Florian Haftmann, Alexander Krauss, Ondřej Kunčar, Tobias Nipkow: Data Refinement in Isabelle/HOL. BibTeX.
- Klaus Aehlig, Florian Haftmann, Tobias Nipkow: A Compiled Implementation of Normalization by Evaluation. BibTeX.
- Florian Haftmann, Tobias Nipkow: Code Generation via Higher-Order Rewrite Systems. BibTeX.
- Florian Haftmann: From Higher-Order Logic to Haskell: There and Back Again. 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 – Combining code generation and deductions
- This is implemented in Isabelle/HOL. For inductive predicates in particular, see Turning inductive into equational specifications
- Section 4.3 – Mastering destructive data structures
- This is somehow complementary to Imperative Functional Programming with Isabelle/HOL.
- Section 4.4 – A quickcheck implementation in Isar
- Beyond the basic mechanism introduced here a lot of extensions are available in Isabelle/HOL thanks to Lukas Bulwahn.
- Section 4.5 – Normalisation by Evaluation
- See A Compiled Implementation of Normalization by Evaluation for a thorough treatment.
- Section 4.6 – Applications of proof terms for code generation
- The issues dealt with here are not mentioned elsewhere in the literature so far. On dictionary construction for proofs see particularly A Mechanized Translation from Higher-Order Logic to Set Theory.
- Section 5.3.1 – Invariants
- See Data Refinement in Isabelle/HOL for the state of the art.
- Section 5.3.3 – Logics other than HOL
- The »partial function« package in Isabelle/HOL demonstrates that it is possible to apply domain theory to specific problems without the need for a different logic with a different function space than HOL. Execution of set theory (ZF) is still an open issue.
- Section 5.4.1 – Further target languages
- Scala has been added as target language.
- Section 5.4.2 – Managing scope and accessibility
- Rudimentary support is available in Isabelle/HOL.
- Section 5.5.1 – Packing machinery
- This is available by the tools »Lifting« and »Transfer«; see Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Section 5.5.2 – Infinite data structures
- Infinite data structures are available through co-datatypes, although their executability is practically restricted to Haskell as target language; see Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
- Section 5.5.3 – Parallelism
- Support for parallel combinators and futures is available using the existing implementation in Isabelle/ML.
- Florian Haftmann, Makarius Wenzel: Local theory specifications in Isabelle/Isar. BibTeX.
- Stefan Berghofer, Lukas Bulwahn, Florian Haftmann: Turning inductive into equational specifications. BibTeX.
- Klaus Aehlig, Florian Haftmann, Tobias Nipkow: A Compiled Implementation of Normalization by Evaluation. BibTeX.
- Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews: Imperative Functional Programming with Isabelle/HOL. BibTeX.
- Florian Haftmann, Donald Kossmann, Eric Lo: A framework for efficient regression tests on database applications. BibTeX.
- Florian Haftmann, Makarius Wenzel: Constructive Type Classes in Isabelle. BibTeX.
- Florian Haftmann, Donald Kossmann, Eric Lo: Parallel Execution of Test Runs for Database Application Systems. BibTeX.
- Florian Haftmann, Donald Kossmann, Alexander Kreutz: Efficient Regression Tests for Database Application Systems. 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.