View source for Extended ML

{{Notability|date=October 2011}}
{{Infobox programming language
| name = Extended ML
| logo = 
| paradigms = [[Programming paradigm|Multi-paradigm]]: [[Functional programming|functional]], [[Imperative programming|imperative]], [[Modular programming|modular]]
| family = [[ML (programming language)|ML]]: [[Standard ML]]
| designers = S. Kahrs, D. Sannella,<br/>A. Tarlecki
| developer = [[University of Edinburgh]]
| released = {{Start date and age|1985}}
| latest release version = 1.1
| latest release date = {{Start date and age|1999}}
| typing = [[Strong and weak typing|strong]], [[Static typing|static]], [[Type inference|inferred]]
| discontinued = Yes
| platform = [[IA-32]], [[SPARC]]
| operating system = [[Cross-platform software|Cross-platform]]: [[Linux]], [[Oracle Solaris|Solaris]]
| license = <!-- [[X License|X]] -->
| website = {{URL|homepages.inf.ed.ac.uk/dts/eml}}<ref>{{cite web |url=https://homepages.inf.ed.ac.uk/dts/eml/ |website=[[University of Edinburgh]] |title=Extended ML |place=Scotland}}</ref>
| implementations = 
| dialects = 
| influenced by=[[ML (programming language)|ML]], [[Standard ML]]
| influenced = 
}}
'''Extended ML''' is a [[General-purpose programming language|general-purpose]], [[High-level programming language|high-level]], [[Wide-spectrum language|wide-spectrum]] [[programming language]] based on the languages [[ML (programming language)|ML]] and [[Standard ML]], covering both [[program specification]] and implementation. It extends the syntax of ML to include [[Axiomatic semantics|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==
{{Reflist}}
*{{Cite book |last1=Sannella |first1=D. |author1-link=Don Sannella |last2=Tarlecki |first2=A. |date=1986 |chapter=Extended ML: an institution-independent framework for formal program development |title=Proceedings of the Workshop on Category Theory and Computer Programming: ETAPS'98 |place=Lisbon, Portugal |publisher=Springer LNCS 240 |volume=173 |issue=2 |pages=364–389}} Workshop in Guildford, England; 1985.
*{{Cite report |last1=Sannella |first1=D. |author1-link=Don Sannella |last2=Tarlecki |first2=A. |date=1989 |title=Toward formal development of ML programs: foundations and methodology; ECS-LFCS-89-71 |place=Edinburgh, Scotland |publisher=Laboratory for Foundations of Computer Science, University of Edinburgh}} Extended abstract in Proceedings of the Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, Springer LNCS, pp. 352, 375–389 (1989).
*{{Cite book |last1=Kahrs |first1=S. |last2=Sannella |first2=D. |author2-link=Don Sannella |last3=Tarlecki |first3=A. |date=1994 |chapter=Interfaces and Extended ML |title=Proceedings of the ACM Workshop on Interface Definition Languages |series=SIGPLAN Notices |place=Portland, Oregon |volume=29 |issue=8 |pages=111–118}}
*{{Cite journal |last1=Kahrs |first1=S. |last2=Sannella |first2=D. |author2-link=Don Sannella |last3=Tarlecki |first3=A. |date=28 February 1997 |title=The definition of extended ML: A gentle introduction |journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]] |volume=173 |issue=2 |pages=445–484|doi=10.1016/S0304-3975(96)00163-6 }}
*{{Cite book |last1=Kahrs |first1=S. |last2=Sannella |first2=D. |author2-link=Don Sannella |date=1998 |chapter=Reflections on the design of a specification language |title=Proceedings of the International Colloquium on Fundamental Approaches to Software Engineering: ETAPS'98 |place=Lisbon, Portugal |publisher=Springer LNCS 1382 |volume=173 |issue=2 |pages=154–170}}
*{{Cite journal |last1=Sannella |first1=D. |author1-link=Don Sannella |last2=Tarlecki |first2=A. |date=1999 |title=Algebraic methods for specification and formal development of programs |journal=[[ACM Computing Surveys]] |volume=31 |issue=3es|page=10 |doi=10.1145/333580.333589 }}

==External links==
*{{Official website|homepages.inf.ed.ac.uk/dts/eml}}, Don Sannella

{{ML programming}}
{{Authority control}}

[[Category:High-level programming languages]]
[[Category:ML programming language family]]
[[Category:Formal specification languages]]
[[Category:1985 software]]
[[Category:Programming languages created in 1985]]


{{Prog-lang-stub}}