Edinburgh LCF was an automatic proof assistant theorem prover designed by Robin Milner for the logic, for reasoning formally using the logic introduced by Scott for domain theory. The functional language ML was originally designed as the metalanguage for designing proof strategies in the system LCF. For instance, the theorem was an abstract data type. Tactics were functions from goals to subgoals. Tactics could fail raising appropriate error messages. As you can see here we have the origin of many of the ingredients of modern Standard ML. Edinburgh ML is in fact the seminal typed call-by-value functional programming language. Its most prominent descendants are Standard ML, as we are going to see today, New Jersey ML which is implemented using the functional abstract machine. The CAML the French version of this language implemented using the categorical abstract machine and other programming languages. In the theorem-proving, proof-checking, proof-assisting tradition, that is the one which was initiated by the LCF system, the most prominent descendants of LCF are HOF, ISABELLE, COQ, LEGO. All of these can be used as logical frameworks.

---