Extended ML

Extended ML
Influenced by
Paradigms	Multi-paradigm: functional, imperative, modular
Family	ML: Standard ML
Designed by	S. Kahrs, D. Sannella, A. Tarlecki
Developer	University of Edinburgh
First appeared	1985; 39 years ago (1985)

Final release	1.1 / 1999; 25 years ago (1999)

Typing discipline	strong, static, inferred
Platform	IA-32, SPARC
OS	Cross-platform: Linux, Solaris
Website	homepages.inf.ed.ac.uk/dts/eml^[1]
ML, Standard ML

Extended ML is a wide-spectrum programming language based on the languages ML and Standard ML, covering both program specification and implementation. It extends the syntax of ML to include axioms, which do not need to be executable but can rigorously specify the behavior of a program. With this addition, the language can be used for stepwise refinement, proceeding gradually from an initial formal specification to eventually yield an executable Standard ML program. Correctness of the final executable with respect to the original specification can then be established by proving the correctness of each of the refinement steps. Extended ML is used for research into and teaching of formal methods in program development and specification, and research into automatic program verification.

Extended ML is neither related to the programming language Extensible ML (other than being similarly derived from ML), nor to the specification language Extensible Markup Language (XML).

References

^ "Extended ML". University of Edinburgh. Scotland.

Kahrs, S.; Sannella, D.; Tarlecki, A. (1994). "Interfaces and Extended ML". Proceedings of the ACM Workshop on Interface Definition Languages. SIGPLAN Notices. Vol. 29. Portland, Oregon. pp. 111–118.{{cite book}}: CS1 maint: location missing publisher (link)
Kahrs, S.; Sannella, D.; Tarlecki, A. (28 February 1997). "The definition of extended ML: A gentle introduction". Theoretical Computer Science. 173 (2): 445–484.
Kahrs, S.; Sannella, D. (1998). "Reflections on the design of a specification language". Proceedings of the International Colloquium on Fundamental Approaches to Software Engineering: ETAPS'98. Vol. 173. Lisbon, Portugal: Springer LNCS 1382. pp. 154–170.
Sannella, D.; Tarlecki, A. (1999). "Algebraic methods for specification and formal development of programs". ACM Computing Surveys. 31 (3es).

External links

Official website, Don Sannella

ML programming

Software

Implementations,
dialects

Caml	OCaml° Eff F*° F#° JoCaml° Reason°
Standard ML	Alice° Extended ML MLton° Standard ML of New Jersey° (SML/NJ)
Dependent ML	ATS°

Concurrent ML
Futhark°
Lazy ML
MacroML
Ur°

Programming tools

Alt-Ergo°

Astrée

Camlp4°

FFTW°

Frama-C°

Haxe°

Marionnet°

MTASC°

Poplog°

Semgrep°

SLAM project

Theorem provers,
proof assistants

Coq°
HOL°
- HOL Light°
Isabelle°
LEGO
Logic for Computable Functions
Matita°
Twelf°

GeneWeb°

Community

Designers	Lennart Augustsson (Lazy ML) Damien Doligez (OCaml) Gérard Huet (Caml) Xavier Leroy (Caml, OCaml) Robin Milner (ML) Don Sannella (Extended ML) Don Syme (F#)