Standard ML

来自维基百科,自由的百科全书

Standard MLSML),是一个函数式指令式模块化[1]通用编程语言,具有编译时间类型检查类型推论[5]。它流行于编译器作者和编程语言研究者和自动定理证明研究者之中。

事实速览 编程范型, 语言家族 ...
Standard ML
编程范型多范型函数式, 指令式, 模块化[1]
语言家族ML
发行时间1983年,​42年前​(1983[2]
型态系统类型推论, 静态, 强类型
文件扩展名.sml
网站Standard ML Family GitHub Project
主要实作产品
SML/NJ, MLton
衍生副语言
Concurrent ML, Dependent ML英语Dependent ML, Alice英语Alice (programming language)
受影响于
ML, Hope, Pascal
影响语言
ATS英语ATS (programming language), Elm, F#, F*, Haskell, OCaml, Python[3], Rust, Scala
关闭

Standard ML是ML的现代方言,ML是用于LCF英语Logic for Computable Functions(可计算函数逻辑)定理证明计划的编程语言。Standard ML在广泛使用的语言之中与众不同,源于它具有正式规定《The Definition of Standard ML》 [4],给出了语言的类型规则英语Type rule操作语义[6]

实现

存在很多SML实现,包括:

标准

  • Standard ML of New Jersey(缩写为SML/NJ),由普林斯顿大学贝尔实验室在1986年开始联合开发的实现,是一个完全的编译器,具有关联的库、工具、交互式外壳和文档,还支持Concurrent ML[7]
  • MLton,是一个全程序优化英语Interprocedural optimization编译器,它产生相比其他ML实现非常快的代码[8]
  • ML Kit[9],由爱丁堡大学Mads Tofte英语Mads Tofte等人在1989年发起开发[10],是一个非常紧密的基于了标准定义的实现,它集成了具有基于区域内存管理英语region-based memory management的垃圾收集器,内存分配指令由编译器推论,可以停用垃圾收集器来支持实时应用。
  • Poly/ML[11],由剑桥大学的David Matthews开发[12],是一个Standard ML的完全的实现,它产生快速代码并支持多核硬件(通过Posix线程);它的运行时间系统,进行并行垃圾收集和不可变子结构的在线共享。
  • HaMLet[13],由MPI-SWS英语Max Planck Institute for Software Systems的Andreas Rossberg编写,是一个SML解释器,意图成为精确且无障碍的标准定义参考实现。
  • Moscow ML[14],是一个轻量级实现,基于了CAML Light运行时引擎。
  • LunarML,产生Lua/JavaScript代码的Standard ML编译器[15]

派生

研究

  • Isabelle/ML,剑桥大学Larry Paulson英语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编译器,它使用有类型的中间语言来优化代码和确保正确性,并可以编译成有类型的汇编语言英语Typed assembly language
  • Poplog英语Poplog系统实现一个版本的SML,还有POP-11英语POP-11、可选的Common LispProlog,允许混合语言编程。

所有这些实现都是开源的并可自由的获得。其中多数用SML实现了自身。不再有任何商业SML实现。

使用SML的项目

证明辅助器HOL4英语HOL (proof assistant)IsabelleLEGO英语LEGO (proof assistant)Twelf英语Twelf是用Standard ML写成。它还用于编译器制作和集成电路设计比如ARM[22]

参见

引用

外部链接

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.