About

code generator Florian Haftmann

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.haftmann_at_informatik.tu-muenchen.de.

Publications

For Scintilla