对于后代,引用自己的答案:
Isabelle本身是在标准ML中实现的,但是为了与外部世界通信,它使用称为PIDE(= Prover IDE)的协议.PIDE的参考实现与Isabelle捆绑在一起并用Scala编写,因此它可以与任何JVM语言一起使用.PIDE的主要应用是Isabelle/jEdit,它使用jEdit编辑器为Isabelle构建一个IDE,包括标记,连续检查,......
通过重用底层协议,您可以在Isabelle之上实现自己的应用程序.
据我所知,目前最先进的例子是Leon,它是Scala程序的自动验证和综合工具包.在内部,它使用libisabelle与Isabelle进行交流.(完全披露:我是libisabelle的作者.)在一篇论文中给出了如何工作的概述.
libisabelle本身作为独立库提供,包括一些基本文档,可以让您开始使用.有关详细信息,请参阅存储库.从本质上讲,它允许你
term"$n > 0 --> ($b & ${HOLogic.True})")中Isabelle术语语法的好东西没有内置的例程来设置目标状态并应用一些证明步骤,但必要的基础设施就在那里.