Version 1.1 is a complete implementation of the Extended ML seen as a 'programming language'. It allows for parsing, type-checking and evaluation of arbitrary EML code, be it pure Standard ML or full-blown EML with its axioms and other specification constructs. All of this is done in a strict adherence to the formally defined EML Syntax, Static Semantics and Dynamic Semantics, as of the EML Definition, version 1.15 + 0.2i. See the file CHANGES for a list of changes to the EML Kit from version 1.0 to 1.1.
Now, there is a great need for an "implementation" of the EML Verification Semantics. We hope the EML Kit will help in as well as benefit from the current work on the EML proof theory, proof obligation generators, prototype provers, etc. Yet, as for now only the syntax and type correctness of axioms is checked by the EML Kit - there is no extra aid in proving them correct, sufficient or whatever.
A big step towards this goal is The EML Kit Proof Obligations Generator - an extension of EML Kit 1.1. It comes with Graphical Pretty Printer for Proof Obligations - an X Window-based browser for proof obligations.
The EML Kit 1.1 Sources Release is intended for everybody (you can fetch the eml11-src.tar.gz archive or look at the README.eml11-src).
The EML Kit 1.1 i386 Binaries Release is for i386 (Linux) users only (you can fetch the eml11-i386.tar.gz archive or look at the README.eml11-i386).
The EML Kit 1.1 SPARC Binaries Release is for Sun SPARC (Solaris) users only (you can fetch the eml11-sparc.tar.gz archive or look at the README.eml11-sparc).
There is also some documentation available. In particular our paper on the EML Kit.
The EML Kit 1.1 Proof Obligations Generator Sources Release is also available (you can fetch the eml11ogen-src.tar.gz archive or look at the README.eml11ogen-src).
The EML Kit 1.1 Proof Obligations Generator i386 Binaries Release is for i386 (Linux) users only (you can fetch the eml11ogen-i386.tar.gz archive or look at the README.eml11ogen-i386).
The Graphical Pretty Printer for Proof Obligations 1.0 Sources Release is available, too (you can fetch the gpp10-src.tar.gz archive or look at the README.gpp10-src).
The Graphical Pretty Printer for Proof Obligations 1.0 i386 Binaries Release is for i386 (Linux) users only (you can fetch the gpp10-i386.tar.gz archive or look at the README.gpp10-i386).
The development of the EML Kit has been partially supported by KBN (Polish State Research Committee) grants " Formal Methods of Software Development" and " Logical Aspects of Software Specification and Development Methods".
The EML Kit is based on the ML Kit; a flexible, clean and modularized interpreter of the Standard ML, written in Standard ML. The EML Kit is no longer maintained. For a more up to date tool, please refer to the page of Extended Moscow ML.
The authors of the EML Kit: Marcin Jurdzinski, Mikolaj Konarski, Slawomir Leszczynski and Aleksy Schubert and the author of the EML Kit Proof Obligations Generator and Graphical Pretty Printer Arkadiusz Bryndza are very grateful for numerous bug-reports and comments (the signs of appreciation were also very helpful :-).