Frequently asked question: I got an email containing a downloadable file having an eml extension. Can you tell me what this means?

Answer: eml is the Microsoft Outlook/mail e-mail file format. Just like Word documents have .doc extensions and Excel spreadsheets have .xls, email files have .eml. You should be able to open .eml files in Outlook. All this has nothing whatsoever to do with EML as described here, and I can't help you with whatever your problem is with your eml attachment.

Extended ML

Extended ML (EML) is a framework for specification and formal development of Standard ML (SML) programs. EML specifications look just like SML programs except that axioms are allowed in signatures and in place of code in structures and functors. Some EML specifications are executable, since SML function definitions are just axioms of a certain special form. This makes EML a "wide-spectrum" language which can be used to express every stage in the development of a SML program from the initial high-level specification to the final program itself and including intermediate stages in which specification and program are intermingled.

Formally developing a program in EML means writing a high-level specification of a generic SML module and then refining this specification top-down by means of a sequence (actually, a tree) of development steps until an executable SML program is obtained. The development has a tree-like structure since one of the ways to proceed from a specification is to decompose it into a number of smaller specifications which can then be independently refined further. In programming terms, this corresponds to implementing a program module by decomposing it into a number of independent sub-modules. The end-product is an interconnected collection of generic SML modules, each with a complete and accurate specification of its interface with the rest of the system. The explicit interfaces enable correct reuse of the individual modules in other systems, and facilitate maintainability by making it possible to localize the effect on the system of subsequent changes in the requirements specification.

This work is complemented by research on algebraic and logical foundations for specification and formal program development. These foundations give substance to guarantees that a formally developed software system satisfies the specification of requirements from which the development process commenced. Look here for more information, and/or read

D. Sannella and A. Tarlecki. Foundations of Algebraic Specification and Formal Software Development. EATCS Monographs in Theoretical Computer Science. Springer, 2012. ISBN 978-3-642-17335-6. Order from Amazon (reviews) or Springer.

Publications

Here are good places to start reading about EML.

• D. Sannella. Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park, 1990. Springer Workshops in Computing, 99-130 (1991).
• S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML: a gentle introduction. Theoretical Computer Science 173:445-484 (1997).

Here are some other papers on EML, in reverse chronological order. (Some of the details in the older papers are obsolete.)

• D. Sannella and A. Tarlecki. Algebraic methods for specification and formal development of programs. ACM Computing Surveys 31 (3es) (1999).
• S. Kahrs and D. Sannella. Reflections on the design of a specification language. Proc. Intl. Colloq. on Fundamental Approaches to Software Engineering, ETAPS'98, Lisbon. Springer LNCS 1382, 154--170 (1998).
• S. Kahrs. On the static analysis of Extended ML. Research note, Laboratory for Foundations of Computer Science, University of Edinburgh (1995).
• S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML. Report ECS-LFCS-94-300, Laboratory for Foundations of Computer Science, University of Edinburgh (1994). A subsequent version of this is here (v1.21, 1997).
  Anyone who wants to try reading this should start with: The definition of Extended ML: a gentle introduction. Theoretical Computer Science 173:445-484 (1997).
• S. Kahrs, D. Sannella and A. Tarlecki. Interfaces and Extended ML. Proc. ACM Workshop on Interface Definition Languages, Portland, Oregon. SIGPLAN Notices 29(8):111-118 (1994).
• S. Kahrs, D. Sannella and A. Tarlecki. The semantics of Extended ML: a gentle introduction. Proc. Intl. Workshop on Semantics of Specification Languages, Utrecht. Springer Workshops in Computing (1993).
  But wait! An improved and extended version of this is: The definition of Extended ML: a gentle introduction. Theoretical Computer Science 173:445-484 (1997).
• D. Sannella and A. Tarlecki. Extended ML: past, present and future. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen, 1990. Springer LNCS 534, 297-322 (1991).
• D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Report ECS-LFCS-89-71, Laboratory for Foundations of Computer Science, University of Edinburgh (1989).
  This is the full version of an extended abstract that appeared in Proc. Joint Conf. on Theory and Practice of Software Development, Barcelona, Springer LNCS 352, 375-389 (1989).
• D. Sannella and A. Tarlecki. Extended ML: an institution-independent framework for formal program development. Proc. Workshop on Category Theory and Computer Programming, Guildford, 1985. Springer LNCS 240, 364-389 (1986).
• D. Sannella. Formal specification of ML programs. Report ECS-LFCS-86-15, Laboratory for Foundations of Computer Science, University of Edinburgh (1986).
• D. Sannella and A. Tarlecki. Program specification and development in Standard ML. Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, 67-77 (1985).

Tool support

An EML parser and typechecker by Kenneth MacKenzie based on Moscow ML v2.0 is available here.

The EML Kit, a parser and typechecker for EML based on the ML Kit, is available from Warsaw. If you experience delays in downloading, try these local copies (version 1.1): eml11-src.tar.gz (source, 300617 bytes) eml11-i386.tar.gz (i386 Linux binaries, 3394292 bytes) eml11-sparc.tar.gz (Sun SPARC Solaris binaries, 4890079 bytes).

Ben Kleinman worked on an environment for formal development of terminating SML programs in EML, building on the EML Kit, a prototype proof obligation generator by Paul Varnish, and the PVS theorem prover, but Ben moved on and that work has been abandoned.

Anybody who is interested in adding support for EML parsing and typechecking to an existing SML implementation is encouraged to read On the static analysis of Extended ML, and to contact me for further support and encouragement.

Educational resources

EML was used until 2010/2011 in the following course at the University of Edinburgh:

• A third-year undergraduate course in Functional Programming and Specification. This is a self-contained introduction to programming in SML and specification in EML.

Until 2000/2001 it was also used in the following course:

• A third-year undergraduate course on Programming Methodology. The SML module system was used to teach programming in the large and EML was used to teach formal specification and verification.

Follow the links to find course notes etc. (If the course is in progress then some of the notes, examples, exercises etc. may be missing; contact me if you need them and can't wait.) Some of the items in the above list of publications are tutorial in character and can be used to teach EML. I would particularly recommend Formal specification of ML programs (an elementary tutorial about specification and proof) and Formal program development in Extended ML for the working programmer (a presentation of EML for people who want to use it without bothering about the theory behind it). Both are unfortunately obsolete with respect to the current syntax of EML, but the differences are minor. See the lecture notes here, here, here and here for a corrected version of the former.

EML is also used or has been used in various courses at other universities. Anybody who would like to publish a link here is invited to contact me.