Jump to content

Extended ML

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by B4hand (talk | contribs) at 15:17, 15 September 2004 (Made link direct). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Extended ML is a programming language created by Kahrs, Sannella and Tarlecki based on the ML programming language. It extends the syntax of ML to include axioms, which may not be executable but can rigorously specify the behavior of the program. With this addition the language can be used for gradual refinement of a program from an initial formal specification into an executable SML program. Extended ML is used for research into and teaching of formal program development and specification, and research into automatic program verification.

Other than being similarly derived from ML, Extended ML is not related to the EML programming language.

References

  • S. Kahrs, D. Sannella, and A. Tarlecki. The definition of extended ML: A gentle introduction. Theoretical Computer Science, 173(2):445-484, 28 Feb 1997