Standard ML

维基百科,自由的百科全书
跳到导航 跳到搜索
Standard ML
编程范型多范型函数式, 指令式, 模块化[1]
语言家族ML
发行时间1983年,​38年前​(1983[2]
穩定版本
Standard ML '97[3]
(1997年,​24年前​(1997
型態系統类型推论, 静态, 强类型
文件扩展名.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[4], Rust, Scala

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

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

实现[编辑]

存在很多SML实现,包括:

标准

派生

研究

  • Isabelle/ML,剑桥大学Larry Paulson英语Larry Paulson开发的Isabelle,将并行Poly/ML集成入交互式定理证明器[17],它具有一个高端的IDE(基于了jEdit),用于官方Standard ML(SML'97)、Isabelle/ML方言和这个证明语言[18]。开始于Isabelle2016,它还有一个源代码级的ML的调试器。
  • CakeML[19],是一个基于了SML实质性子集的语言,它实现为x86-64机器码的REPL,带有正式验证的运行时间库和到汇编代码的转换。
  • TILT[20],是一个完全验证了的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[21]

参见[编辑]

引用[编辑]

  1. ^ 1.0 1.1 David MacQueen. Modules for Standard ML. LFP '84 Proceedings of the 1984 ACM Symposium on LISP and functional programming. August 1984: 198–207. 
    David Macqueen. An Implementation of Standard ML Modules. 1988. 
  2. ^ Robin Milner. A Proposal for Standard ML (PDF). 1983. 
    Robin Milner, Robert Harper, David B. MacQueen. Standard ML: Report ECS-LFCS-86-2 (PDF). 1986.  School of Informatics Laboratory for Foundations of Computer Science, Edinburgh University.
  3. ^ 3.0 3.1 Milner, Robin; Tofte, Mads; Harper, Robert; MacQueen, David. The Definition of Standard ML (Revised) (PDF). MIT Press. 1997. ISBN 0-262-63181-4. 
  4. ^ itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation. docs.python.org. [2020-04-25]. (原始内容存档于2020-06-14). 
  5. ^ Damas, Luis; Milner, Robin. Principal type-schemes for functional programs (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM: 207–212. 1982. ISBN 978-0-89791-065-1. doi:10.1145/582153.582176. 
    Damas, Luis. Type Assignment in Programming Languages (PDF) (PhD论文). University of Edinburgh. 1985. hdl:1842/13555. CST-33-85. 
  6. ^ Cardelli, Luca. Type Systems (PDF). ACM Computing Surveys. March 1996, 28 (1): 263–264. doi:10.1145/234313.234418. 
  7. ^ smlnj.org. [2020-04-25]. (原始内容存档于2020-05-01). 
  8. ^ mlton.org. [2020-09-27]. (原始内容存档于2020-08-28). 
  9. ^ ML Kit页面存档备份,存于互联网档案馆
  10. ^ Lars Birkedal, Nick Rothwell, Mads Tofte, David N. Turner. The ML Kit, Version 1. 1993. 
  11. ^ Poly/ML页面存档备份,存于互联网档案馆
  12. ^ David Matthews. An Implementation of Standard ML in Poly. 1986. 
  13. ^ HaMLet页面存档备份,存于互联网档案馆
  14. ^ Moscow ML
  15. ^ SML#页面存档备份,存于互联网档案馆
  16. ^ SOSML页面存档备份,存于互联网档案馆
  17. ^ Isabelle页面存档备份,存于互联网档案馆
  18. ^ The Isabelle/Isar Implementation (PDF). 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. 
  19. ^ CakeML页面存档备份,存于互联网档案馆
  20. ^ TILT页面存档备份,存于互联网档案馆
  21. ^ Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli. The Semantics of Power and ARM Multiprocessor Machine Code (PDF). DAMP 2009: 13–24. 

外部链接[编辑]