ML (プログラミング言語)
デイナ・スコットの提案したPPLAMBDAという論理体系を利用し、ロビン・ミルナーはLogic for Computable Functions(英語版) (LCF) という証明のチェックや定理の自動証明をするシステムを実装した。1973年に発足したEdinburgh LCFのプロジェクトにおいて、証明の道筋を関数として記述するためのメタ言語として開発されたのが、MLの最初であり、強い型付きの言語として設計された。
Edinburgh LCFとMLは、1975~76年にエディンバラ大学で実装された。特に1980年代以降、汎用プログラミング言語として多数の機能やライブラリが追加されている。
(この節 参考文献『新しいプログラミング・パラダイム』(ISBN 4-320-02493-1) pp. 120-121)