OpenProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. OpenProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL.
released on 13 March 2016
|License||Verified by||Verified on||Notes|
|GPLv2||Deborah Nicholson||23 June 2008|
Leaders and contributors
Resources and communication
This entry (in part or in whole) was last reviewed on 19 January 2017.