This library allows to control an Isabelle process from a Scala application. It allows to interact with the Isabelle process, manipulate objects such as terms and theorems as if they were local Scala objects, and execute ML code in the Isabelle process. The library serves a similar purpose as the discontinued libisabelle.
For information how to setup the library, examples, and documentation, see the website.
- qrhl-tool – A theorem prover for post-quantum security.
- PISA - A reinforcement learning environment for theorem proving in Isabelle.
Development was supported by the Air Force Office of Scientific Research (AOARD Grant FA2386-17-1-4022), by the ERC consolidator grant CerQuS (819317), and by the PRG946 grant from the Estonian Research Council.