Dominique Clément, Joëlle Despeyroux, Th. Despeyroux, Gilles Kahn. A Simple Applicative Language: Mini-ML. In LISP and Functional Programming. pages 13-27, 1986.
This paper presents a formal description of the central part of the ML language in Natural Semantics. Static semantics, dynamic semantics, and translation to an abstract machine code are covered. The description has been tested on a computer and we explain why this is feasible. Several facts that one may want to prove about the language are expressed and proved within the formalism.