歴史的背景

歴史を調べないと分からない処理系、てのも困ったもんだが、

• エジンバラLFが「ロジカルフレーム」として先行か？
• λPrologってのもある。
• スコットのLCF理論が背景
• ミルナーのMLで実装
• CoqはIsabelleの後: Isabelle 1986年、Coq 1989年 3年後

[追記]
"Logic of Computable Functions"は Dana Scott in 1969, "Logic for Computable Functions"は、 Robin Milner 1972。Milnerは1972年にLCFの論文書いている。エジンバラLCFの実装も1972らしい。MLもエジンバラLCFと同時期だろう。なお、ケンブリッジLCFつうのもあるらしい。

Standard MLの規格書は1990年に初版が出版され、1997年に単純化された改版、つうことだが、ポールソンのfoundation論文（1990年くらい？）で既にSMLへの言及があるな。
[/追記]