Re: [isabelle] soundness of Isabelle/HOL

Sorry - Jitawa is the verified runtime. The self-verifying prover on top of
it is called Milawa (

On Mon, Jan 30, 2012 at 10:45 AM, Ramana Kumar <rk436 at> wrote:

> HOL Zero ( was mentioned
> already.
> HOL Light has had some self-verification applied (
> Jitawa is a theorem prover verified in HOL (
> For more about the idea you mentioned, parsing "False" as "True", see
> Pollack Inconsistency (
> On Mon, Jan 30, 2012 at 10:26 AM, Lars Noschinski <noschinl at>wrote:
>> On 30.01.2012 10:59, Matthias Schmalz wrote:
>>> I already know that Isabelle follows the LCF approach and that HOL is
>>> built from a modest number of axioms using conservative extension
>>> methods. It is therefore very likely that proofs by Isabelle are
>>> correct. I also know that this soundness guarantee is restricted to the
>>> inference core; for example, nothing prevents users from configuring the
>>> parser to parse "False" as "True" and therefore giving the impression
>>> that "False" can be proved. (And of course, soundness rests on the
>>> assumption that compiler, ML libraries, operating system, and hardware
>>> behave correctly.)
>> I think HOL Zero tries to make sure that you cannot reconfigure parser
>> and pretty-printer in a way that confuses the user. If you search for
>> mark at on this list, you should find some
>> discussion on this topic.
>>  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.