Standard ML is a safe, modular, strict, functional,
polymorphic programming language with compile-time type checking and
type inference, garbage collection, exception handling, immutable data
types and updatable references, abstract data types, and parametric
modules. It has efficient implementations and a formal definition with
a proof of soundness.