Tag: robin-milner

ML began as the metalanguage of the LCF theorem prover and introduced practical polymorphic type inference, showing that strong static typing could coexist with concise functional programs.

LCF made a small trusted proof kernel the foundation of an extensible interactive theorem prover, while its ML metalanguage gave users a programmable way to construct proof tactics without expanding the trusted base.