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.


[0] https://isabelle.in.tum.de/overview.html
[1] http://lars.hupel.info/libisabelle/
[2] https://github.com/larsrh/libisabelle

--
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 https://groups.google.com/d/optout.