libisabelle: A Scala library which talks to Isabelle

Previous Topic Next Topic
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view

libisabelle: A Scala library which talks to Isabelle

Lars Hupel-2
Isabelle is an interactive theorem prover. It is used for formal specification & proofs. An overview can be found on its website [0]. Some of the readers of this list might be familiar with Coq; both systems serve similar purposes. The main mode of interaction with Isabelle is via its IDE; users type in specifications and proofs which are being checked continuously. It offers automated proof and disproof methods, various decision procedures, executable code generation, a rich library of classical mathematics and much more.

Isabelle ships with a Scala API ("PIDE") tailored for interactive use in its IDE. To cater for different kinds of applications, libisabelle [1] provides a high-level wrapper around this API. Notable features include:
  • (mostly) asynchronous API
  • prover interaction abstracted into typed, atomic operations
  • automatic installation of Isabelle
  • multi-version and multi-tenancy support
Apart from the Isabelle-Leon integration (see my other mail to this list from today), libisabelle has been used in a project for educational mathematical software and in an ongoing effort for code clone detection in Isabelle sources.

Source code is available on GitHub [2]. If you have any kind of software which could benefit from the ability to formally prove or check assertions, I'd be happy to hear about your use case.


You received this message because you are subscribed to the Google Groups "scala-announce" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
For more options, visit