On Sun, 6 May 2012, Ramana Kumar wrote:
> For the record, OpenTheory (http://www.gilith.com/research/opentheory/)
> is also an independent implementation of HOL, and may be treated as a
> separate proof checker. It wasn't written with the same soundness goals
> as HOL Zero, though; I would still recommend HOL Zero for checking when
> soundness is a major concern.
Just browsing through the opentheory 1.1 sources a bit, I find it more
re-assuring as independent checker, even if it is not designed for that.
It has:
* Standard ML with its no-sense semantics
* support for 3 independent SML compilers
* fixed input format -- no arbitrary user code accessing the platform
Even the usual fine points of SML programming have been observed
carefully:
* avoidance of unspecific exception handlers -- no dreaded
"handle _ => ..." that would let bad weather intrude program semantics
(I've seen this occasionally in the HOL Zero sources)
* "critical" wrappers for the (very few) accesses to global
state variables (apparently stemming from the Metis adaption to
multithreaded Isabelle/ML)
Makarius
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
