|
|
|
|
|
by more_original
3457 days ago
|
|
It's Meta Language. The ML language was developed in the early 1970s as a meta-language for the LCF theorem prover. ML was developed as a language for programming proof tactics. The strong type system and type soundness guarantees of ML were important to guarantee that such tactics could only prove correct theorems. https://en.wikipedia.org/wiki/ML_(programming_language) |
|
http://sml-family.org/sml97-defn.pdf