Robert Soeldner (Jan 12 2024 at 12:54): Robert Soeldner (Jan 12 2024 at 12:54):Are there existing binary (executable) applications which have been built on top of Isabelle/HOL, such as a Web-based tool to verify properties of a DSL? I've seen new keywords to work within the Isabelle distribution (i.e. JEdit) but are there standalone binaries?
Yutaka Nagashima (Jan 13 2024 at 01:33):Robert Soeldner said:
Are there existing binary (executable) applications which have been built on top of Isabelle/HOL, such as a Web-based tool to verify properties of a DSL? I've seen new keywords to work within the Isabelle distribution (i.e. JEdit) but are there standalone binaries?
I have a faint recollection that Cezary may have worked on something similar in the past.
If my memory serves me right, his web interface was compatible with both HOL4 and Isabelle/HOL.
However, I'm not entirely sure, so please take this with a grain of caution.
http://cl-informatik.uibk.ac.at/cek/
Mathias Fleury (Jan 13 2024 at 07:55):Is something like https://www.tu.berlin/mtv/forschung/software/proofbuddy which is different interface to Isabelle what you are looking for?
Last updated: May 02 2024 at 12:29 UTC