Dependent ML

在2020年末尾时，在版本110.99发行中增加了64-bit支持。 Extended ML（英语：Extended ML） Dependent ML（英语：Dependent ML） Standard ML of New Jersey License. www.smlnj.org. [2021-09-24]

Standard ML（SML），是一个函数式、指令式、模块化的通用的编程语言，具有编译时间类型检查和类型推论。它流行于编译器作者和编程语言研究者和自动定理证明研究者之中。 Standard ML是ML的现代方言，ML是用于LCF（英语：Logic for Computable

Pfenning（英语：Frank Pfenning）提出的Dependent ML（英语：Dependent ML）发展而来，它向ML扩展了依赖类型。 F#，由微软研究院（MSR）开发，是一个基于OCaml的一个以.NET为目标的编程语言。 F*，由MSR和INRIA主导开发，是一个基于ML的依赖类型函数式编程语言。

量词和存在量词；在依赖类型函数式编程语言如ATS（英语：ATS (programming language)）、Agda、Dependent ML（英语：Dependent ML）、Epigram（英语：Epigram (programming language)）、F*和Idris中，依赖类型系统

F*（读作“F star”）是一个由微软研究院和INRIA主导开发的、基于ML的依赖类型函数式程序语言，主要用于程序的形式化验证。 F*的类型系统十分丰富，支持依赖类型、单子化效用（monadic effects）和细化类型（refinement types）。这使其能够准确地用于表述程序的形式化规范，包括功能正确性和安全性。