Efficient Regression Tests for Database Applications. - Florian Haftmann; Donald Kossmann; Alexander Kreutz (CIDR, 2005)

Parallel Execution of Test Runs for Database Application Systems. - Florian Haftmann; Donald Kossmann; Eric Lo 001 (VLDB, 2005)

Constructive Type Classes in Isabelle. - Florian Haftmann; Makarius Wenzel (TYPES, 2006)

A framework for efficient regression tests on database applications. - Florian Haftmann; Donald Kossmann; Eric Lo 001 (VLDB J., 2007)

A Compiled Implementation of Normalization by Evaluation. - Klaus Aehlig; Florian Haftmann; Tobias Nipkow (TPHOLs, 2008)

Imperative Functional Programming with Isabelle/HOL. - Lukas Bulwahn; Alexander Krauss 001; Florian Haftmann; Levent Erkök; John Matthews (TPHOLs, 2008)

Local Theory Specifications in Isabelle/Isar. - Florian Haftmann; Makarius Wenzel (TYPES, 2008)

Turning Inductive into Equational Specifications. - Stefan Berghofer; Lukas Bulwahn; Florian Haftmann (TPHOLs, 2009)

Code generation from specifications in higher-order logic. - Florian Haftmann (2009)

Code Generation via Higher-Order Rewrite Systems. - Florian Haftmann; Tobias Nipkow (FLOPS, 2010)

From higher-order logic to Haskell: there and back again. - Florian Haftmann (PEPM, 2010)

CTP-based programming languages?: considerations about an experimental design. - Florian Haftmann; Cezary Kaliszyk; Walther Neuper (ACM Commun. Comput. Algebra, 2010)

A compiled implementation of normalisation by evaluation. - Klaus Aehlig; Florian Haftmann; Tobias Nipkow (J. Funct. Program., 2012)

Data Refinement in Isabelle/HOL. - Florian Haftmann; Alexander Krauss 001; Ondrej Kuncar; Tobias Nipkow (ITP, 2013)

Discrete Summation. - Florian Haftmann (Arch. Formal Proofs, 2014)