Re: [isabelle] Isabelle Foundation & Certification
On Sun, 20 Sep 2015, "Mark Adams" wrote:
Wouldn't it be highly relevant to include HOL Zero in the systems you
consider in your list?
Here is the missing entry:
** HOL Zero **
Minimalistic re-implementation of HOL, designed with trustworthiness as
its top priority.
[ML] Unlike HOL-Light there are explicit provisions to avoid unsafe
aspects of OCaml. Architectural weaknesses remain, since user ML scripts
operate directly on the OCaml toplevel.
[small], [thm], [defs], [context], [logic] similar to HOL Light.
I.e. it is mostly like HOL Light, but [ML] gets ++ (like HOL4 with its SML
basis), because extra care is taken to avoid weaknesses of OCaml.
A fully managed ML environment as in Isabelle would get +++.
This archive was generated by a fusion of
Pipermail (Mailman edition) and