Poly/ML

Poly/ML 是一种高级（但鲜为人知）的 Standard ML 实现。它拥有一个快速的编译器，可在运行时生成高效的机器代码：即运行中的程序可即时“求值”新的 SML 源代码。通过原生线程、互斥锁和条件变量支持多核硬件。其运行时系统执行并行垃圾回收，并实现不可变子结构的在线共享。调试器默认通过命令行工作，但也可集成到现有 IDE 中。编译器的静态阶段可为 IDE 生成标记信息，例如警告、错误、标识符作用域以及子表达式的推断类型。Poly/ML 是大型定理证明项目（尤其是 Isabelle 和 HOL4）的首选 SML 实现。