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 AT truthmachine DOT demon DOT co DOT 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. More recently David Matthews has continued to develop Poly/ML. The Standard Basis Library has been implemented and the compiler converted to the 1997 Definition of Standard ML (Revised). This work was supported in part by LFCS. The most recent work has been rewriting the run-time system which has resulted in the version 5 release. This work was supported by the Verisoft project and the Technical University of Munich.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
- Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael: The verified CakeML compiler backend (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Andronick, June; Lewis, Corey; Matichuk, Daniel; Morgan, Carroll; Rizkallah, Christine: Proof of OS scheduling behavior in the presence of interrupt-induced concurrency (2016)
- Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
- Aransay, Jesús; Divasón, Jose: Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm (2015)
- Rahli, Vincent: Skalpel: a type error slicer for standard ML (2015)
- Bella, Giampaolo: Inductive study of confidentiality: for everyone (2014) ioport
- Hupel, Lars: Interactive simplifier tracing and debugging in Isabelle (2014)
- Wenzel, Makarius: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit (2012)
- Dos Reis, Gabriel; Matthews, David; Li, Yue: Retargeting OpenAxiom to Poly/ML: towards an integrated proof assistants and computer algebra system framework (2011)