Standard ML：はじめに

Isabelle2016をインストールしたら、PolyMLが付いていた、つうか、PolyMLはIsabelleの実装言語。PolyMLはStandard MLの実装。

PolyMLのFAQ http://www.polyml.org/FAQ.html によると、IsabelleとPolyMLの歴史はほぼ一緒らしい。https://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29 によると、"Initial release 1986" なので、今年でちょうど30年になる。PolyMLも同様の歴史だろう。十分に枯れた処理系だ。

PolyというMLライクな言語があり、PolyMLはPolyで実装されたStandard MLだったが、後でStandard MLで実装されたStandard MLになったようだ。

Isabelle2016/contrib/polyml-5.6-1/ にPolyMLが入っている。PolyML自体の最新バージョンも Version 5.6 。

PolyML自体の使い方の情報は少ない。SML/NJの情報が多いようだ。調べてみた結果を[StandardML]タグでメモしていく。