Standard ML(SML),是一个函数式、指令式、模块化[1]的通用的编程语言,具有编译时间类型检查和类型推论[5]。它流行于编译器作者和编程语言研究者和自动定理证明研究者之中。
Quick Facts 编程范型, 语言家族 ...
Standard ML编程范型 | 多范型:函数式, 指令式, 模块化[1] |
---|
语言家族 | ML |
---|
发行时间 | 1983年,41年前(1983)[2] |
---|
型态系统 | 类型推论, 静态, 强类型 |
---|
文件扩展名 | .sml |
---|
网站 | Standard ML Family GitHub Project |
---|
|
SML/NJ, MLton |
|
Concurrent ML, Dependent ML, Alice |
|
ML, Hope, Pascal |
|
ATS, Elm, F#, F*, Haskell, OCaml, Python[3], Rust, Scala |
Close
Standard ML是ML的现代方言,ML是用于LCF(可计算函数逻辑)定理证明计划的编程语言。Standard ML在广泛使用的语言之中与众不同,源于它具有正式规定《The Definition of Standard ML》
[4],给出了语言的类型规则和操作语义[6]。
存在很多SML实现,包括:
标准:
派生:
研究:
- Isabelle/ML,剑桥大学的Larry Paulson开发的Isabelle,将并行Poly/ML集成入交互式定理证明器[18],它具有一个高端的IDE(基于了jEdit),用于官方Standard ML(SML'97)、Isabelle/ML方言和这个证明语言[19]。开始于Isabelle2016,它还有一个源代码级的ML的调试器。
- CakeML[20],是一个基于了SML实质性子集的语言,它实现为x86-64机器码的REPL,带有正式验证的运行时间库和到汇编代码的转换。
- TILT[21],是一个完全验证了的SML编译器,它使用有类型的中间语言来优化代码和确保正确性,并可以编译成有类型的汇编语言。
- Poplog系统实现一个版本的SML,还有POP-11、可选的Common Lisp和Prolog,允许混合语言编程。
所有这些实现都是开源的并可自由的获得。其中多数用SML实现了自身。不再有任何商业SML实现。
证明辅助器HOL4、Isabelle、LEGO和Twelf是用Standard ML写成。它还用于编译器制作和集成电路设计比如ARM[22]。
The Isabelle/Isar Implementation (PDF). [2021-09-01]. (原始内容 (PDF)存档于2021-09-01). Isabelle/ML is best understood as a certain culture based on Standard ML. Thus it is not a new programming language, but a certain way to use SML at an advanced level within the Isabelle environment. This covers a variety of aspects that are geared towards an efficient and robust platform for applications of formal logic with fully foundational proof construction — according to the well-known LCF principle. There is specific infrastructure with library modules to address the needs of this difficult task.