This section of the website is meant to improve the Isabelle platform for Interactive Theorem Proving, as far as I am personally involved. Beyond that there are many users, contributors, and developers of Isabelle applications and add-on components world-wide, e.g. see the collected outcomes in the Archive of Formal Proofs as the visible universe of formally published results.

The category proposals collects articles on particular topics as they emerge over time. This may serve informative purposes on important lines of further Isabelle development, or as a starting point for discussion and elaboration — depending on specific demands of big and important applications out there.

Moreover, this is an explicit invitation to support proposals actively. A variety of ways are possible to do that:

• Donate small amounts, potentially dedicated to a particular area of work that you want to see raised in priority. This may be understood as a modest form of crowdfunding.
• Procure some funding as part of a bigger research or development project, and get me involved as an external contractor or consultant.
• Invite me to your research or development group (at your expenses), in order to support you, your co-workers, your students, your users in advanced Isabelle applications. For example, the format could be an internal workshop of a few days, or a stay over a few weeks, to instruct prospective experts of Isabelle tool development.
• More ambitious plans according to your particular requirements and possibilities.

I am ready to provide such professional services around the Isabelle platform that fit into my areas of expertise, and can be fulfilled with the side-condition of myself being mainly located at the center of Europe: Bavaria / Swabia / Augsburg. 2000 years ago that was the capital of the Roman province of Raetia. 500 years ago it was the commercial and financial center of the Western World (the Empire of Charles V), due to the Fugger family. Today it is my own base for research and development projects, where I am both remote and connected to the world.

Please contact me via email as given on the main page. Further local address details are given in the impressum (together with some formal German legalese).