HOL4 workshop at CADE-25

The HOL4 workshop will happen on Sunday 02-Aug-2015 and Monday 03-Aug-2015 in Berlin, as an associated event of the 25th International Conference on Automated Deduction (CADE-25). The main theme are future directions and visions on HOL4 development: both users and developers are invited to participate in the discussion.

Even though I am myself not an HOL4 person, I will give a presentation about Isabelle/PIDE/jEdit as integrated development environment for Standard ML. The abstract is as follows:

After more than 7 years of development, Isabelle/PIDE/jEdit is today the standard way to interact with that particular proof assistant. In Isabelle2015 (May 2015) the TTY-based REPL and its wrapper for Proof General / Emacs have already been dismantled. This radical move might be taken as an opportunity of the HOL4 community to attract former Isabelle users who really do want to use plain TTY interaction. Or as an opportunity to discuss possibilities for HOL4 users and developers to make their own moves towards full-scale IDE support.

As a very modest start, I would like to present various possibilities of Isabelle/PIDE to operate as IDE for Standard ML, which happens to be the underlying language platform of HOL4 as well. This touches various facilities of Poly/ML that David Matthews provides specifically to tool builders: run-time compiler invocation with IDE feedback, toplevel environment management, structured toplevel printing (with markup and hyperlinks), and potentially also run-time debugging of SML (still unused in Isabelle2015).

Beyond that it is also possible to integrate any other languages that are related or unrelated to the prover platform, using PIDE libraries either on the ML or Scala side of that IDE framework.