Standard ML
脚本错误:没有“Infobox”这个模块。脚本错误:没有“Check for unknown parameters”这个模块。 Standard ML(SML),是一个函数式、指令式、模块化[1]的通用的编程语言,具有编译时间类型检查和类型推论[2]。它流行于编译器作者和编程语言研究者和自动定理证明研究者之中。
Standard ML是ML的现代方言,ML是用于Template:Le(可计算函数逻辑)定理证明计划的编程语言。Standard ML在广泛使用的语言之中与众不同,源于它具有正式规定《The Definition of Standard ML》 [3],给出了语言的Template:Le和操作语义[4]。
实现[编辑]
存在很多SML实现,包括:
标准:
- Standard ML of New Jersey(缩写为SML/NJ),由普林斯顿大学和贝尔实验室在1986年开始联合开发的实现,是一个完全的编译器,具有关联的库、工具、交互式外壳和文档,还支持Concurrent ML[5]。
- MLton,是一个Template:Le编译器,它产生相比其他ML实现非常快的代码[6]。
- ML Kit[7],由爱丁堡大学的Template:Le等人在1989年发起开发[8],是一个非常紧密的基于了标准定义的实现,它集成了具有Template:Le的垃圾收集器,内存分配指令由编译器推论,可以停用垃圾收集器来支持实时应用。
- Poly/ML[9],由剑桥大学的David Matthews开发[10],是一个Standard ML的完全的实现,它产生快速代码并支持多核硬件(通过Posix线程);它的运行时间系统,进行并行垃圾收集和不可变子结构的在线共享。
- HaMLet[11],由Template:Le的Andreas Rossberg编写,是一个SML解释器,意图成为精确且无障碍的标准定义参考实现。
- Moscow ML[12],是一个轻量级实现,基于了CAML Light运行时引擎。
- LunarML,产生Lua/JavaScript代码的Standard ML编译器[13]。
派生:
- SML#[14],是日本东北大学Template:Le开发的SML家族新语言,提供了记录多态性和C语言互操作性。它是常规的本机编译器,名字的“#”号不暗示着要在.NET框架上运行。
- Template:Le,Alice ML是萨尔兰大学开发的基于Standard ML的函数式编程语言,它增加了惰性求值、并发性(多线程和通过远程过程调用的分布式计算)和约束编程特征。
- SOSML[15],是用TypeScript写的SML实现,可以直接运行在web浏览器内。它实现了大多数SML语言和选择的部分SML基本库。
研究:
- Isabelle/ML,剑桥大学的Template:Le开发的Isabelle,将并行Poly/ML集成入交互式定理证明器[16],它具有一个高端的IDE(基于了jEdit),用于官方Standard ML(SML'97)、Isabelle/ML方言和这个证明语言[17]。开始于Isabelle2016,它还有一个源代码级的ML的调试器。
- CakeML[18],是一个基于了SML实质性子集的语言,它实现为x86-64机器码的REPL,带有正式验证的运行时间库和到汇编代码的转换。
- TILT[19],是一个完全验证了的SML编译器,它使用有类型的中间语言来优化代码和确保正确性,并可以编译成Template:Le。
- Template:Le系统实现一个版本的SML,还有Template:Le、可选的Common Lisp和Prolog,允许混合语言编程。
所有这些实现都是开源的并可自由的获得。其中多数用SML实现了自身。不再有任何商业SML实现。
使用SML的项目[编辑]
证明辅助器Template:Le、Isabelle、Template:Le和Template:Le是用Standard ML写成。它还用于编译器制作和集成电路设计比如ARM[20]。
参见[编辑]
引用[编辑]
- ↑ 引用错误:
<ref>标签无效;未给name(名称)为“module”的ref(参考)提供文本 - ↑ 脚本错误:没有“citation/CS1”这个模块。
Template:Cite thesis - ↑ Template:Cite web
- ↑ Template:Cite journal
- ↑ Template:Cite web
- ↑ Template:Cite web
- ↑ ML Kit(页面存档备份,存于互联网档案馆)
- ↑ Template:Cite web
- ↑ Poly/ML(页面存档备份,存于互联网档案馆)
- ↑ Template:Cite web
- ↑ HaMLet(页面存档备份,存于互联网档案馆)
- ↑ Template:Cite web
- ↑ Template:Cite web
- ↑ SML#(页面存档备份,存于互联网档案馆)
- ↑ SOSML(页面存档备份,存于互联网档案馆)
- ↑ Isabelle(页面存档备份,存于互联网档案馆)
- ↑ Template:Cite web
- ↑ CakeML(页面存档备份,存于互联网档案馆)
- ↑ TILT(页面存档备份,存于互联网档案馆)
- ↑ 脚本错误:没有“citation/CS1”这个模块。
外部链接[编辑]
- Standard ML Family GitHub Project(页面存档备份,存于互联网档案馆)
- Programming in Standard ML(页面存档备份,存于互联网档案馆)
- cmlib - A basic library of algorithms and data structures (a la NJlib) (页面存档备份,存于互联网档案馆)
- SML Help (页面存档备份,存于互联网档案馆)
- Awesome Standard ML (页面存档备份,存于互联网档案馆)
- Programming in Standard ML '97: An On-line Tutorial(页面存档备份,存于互联网档案馆)
- CSE341: Programming Languages(页面存档备份,存于互联网档案馆), Dan Grossman, University of Washington.
- COMP 105 pages: Learning Standard ML (页面存档备份,存于互联网档案馆)
脚本错误:没有“Navbox”这个模块。