scala-isabelle

What is this library for?

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.

Further reading

For information how to setup the library, examples, and documentation, see the website.

Projects using scala-isabelle

• qrhl-tool – A theorem prover for post-quantum security.
• PISA - A reinforcement learning environment for theorem proving in Isabelle.

Acknowledgments

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.