伊莎贝尔和斯卡拉[关闭]

我正在考虑创建 Eclipse PDE，并且需要与 Isabelle 进行通信。我确实发现一些出版物声称 Scala 可用于与 Isabelle 进行通信。

我正在寻找如何使用 Scala 在 Isabelle 中创建证明的示例。

为了后代，引用我自己较旧的答案 https://stackoverflow.com/a/30934839/4776939:

Isabelle 本身是用标准 ML 实现的，但为了与外部世界进行通信，它使用了一种名为PIDE（= 证明者 IDE）。 PIDE 的参考实现与 Isabelle 捆绑在一起并用 Scala 编写，因此它可以与任何 JVM 语言一起使用。 PIDE的主要应用是Isabelle/jEdit，它使用jEdit编辑器为Isabelle构建一个IDE，包括标记、连续检查、...

通过重用底层协议，您可以在 Isabelle 之上实现您自己的应用程序。

据我所知，目前最先进的例子是Leon http://lara.epfl.ch/w/leon，这是一个用于 Scala 程序的自动验证和综合工具包。在内部，它使用利比萨贝尔 https://github.com/larsrh/libisabelle与伊莎贝尔交流。（全面披露：我是《libisabelle》的作者。）其工作原理的概述见a paper https://arxiv.org/abs/1607.01539.

libisabelle 本身可作为独立库使用，其中包括一些可以帮助您入门的基本文档。看存储库 https://github.com/larsrh/libisabelle更多细节。从本质上讲，它允许您

• 从 Scala 中管理 Isabelle 安装（下载、解压）
• 不同 Isabelle 版本的摘要（当前支持：2016 和 2016-1 候选版本）
• Isabelle 会话的生命周期管理（构建、启动、停止）
• 将 Isabelle/ML 函数视为 Scala 函数
• Scala 中的 Isabelle 术语语法等好东西（term"$n > 0 --> ($b & ${HOLogic.True})")

没有内置例程来设置目标状态并应用一些证明步骤，但必要的基础设施都在那里。