Polyml.org
Title
Poly/ML Home Page
Description
History and Acknowledgements
Poly/ML was originally written by David Matthews at the Computer Laboratory at Cambridge University. It was written in an experimental language, Poly, similar to ML but with a different type system. Among the first users was Larry Paulson who used it to develop the Isabelle theorem prover. It was licensed by Cambridge University's company Cambridge University Technical Services, then called Lynxvale, to Abstract Hardware Limited (AHL) who developed it further and used it to write the Lamba system for hardware verification as well as other tools. Mike Crawley did significant work on the run-time system and Simon Finn was heavily involved in translating Poly/ML from Poly into Standard ML. Nick Chapman (nic @ truthmachine.demon.co.uk) wrote the C-language interface. In 1999 AHL's rights in Poly/ML were acquired by CUTS and they agreed to make Poly/ML freely available.
Early last year David Matthews started on the implementation of the Standard Basis Library and the conversion to the 1997 Definition of Standard ML (Revised). This work was supported in part by LFCS.
How much of Standard/ML does Poly/ML support?
Since the version 4.0 release Poly/ML now supports the full version of the language as given in the "Definition of Standard ML (Revised)", generally known as ML97.
Contact
- David Matthews
-
- Edinburgh -
- United Kingdom of Great Britain and Northern Ireland EH4 3BB
-
- +4.4
