3 Feb
2026
3 Feb
'26
12:47 p.m.
On 03/02/2026 07:24, Duke Normandin wrote:
Still waiting for Paulson's book to arrive, although I suspect that I might have been too impulsive in buying the book so soon.
You can download the book here: https://www.cl.cam.ac.uk/~lp15/MLbook
It was once very influential to the Interactive Theorem Prover community many decades ago, as far as Standard ML is concerned. Now it is rather dated, not to say archaic.
When I browse today, I learn many things about approaches from distant past. Now, I would do it quite differently, e.g. see the vast Isabelle/ML codebase, with its main library in Isabelle/Pure.
Makarius