[isabelle] Pollack-consistency (HOL Light, Isabelle, and others); Introductions to HOL4 and HOL Zero



Dear List Members,

Through Mark Adams' paper "HOL Zero's Solutions for Pollack-Inconsistency" 
(2016) linked at the HOL Zero homepage, I became aware of the notion of 
Pollack-consistency coined by Freek Wiedijk for the property of "a system being 
able to correctly parse formulas that it printed itself":

	Freek Wiedijk: Pollack-inconsistency
	http://doi.org/10.1016/j.entcs.2012.06.008
	http://www.cs.kun.nl/~freek/pubs/rap.pdf

It is amusing to see how the parsing and printing functions of John's HOL Light 
are put on the rack and stretched quite a bit.
Also Isabelle and other systems are examined.

The interesting point for me was to see that somebody had the same idea. In the 
R0 implementation, not only a formula, but whole printed proofs can be parsed 
again. In fact, if it is compiled and started with "make check", R0 loops 
through all proofs, and this is done twice, with the output of the first run as 
the input of the second, stopping immediately with an error message if a proof 
fails or if the output of the two runs differ. This was implemented quite 
early, so the system was designed from the very beginning to comply with a 
notion of Pollack-consistency not only in terms of formulae, but in terms of 
whole proofs. Like for HOL Zero, this was done in order "to achieve the highest 
levels of reliability and trustworthiness through careful design and 
implementation of its core components" - quoted from:

	Mark Adams: HOL Zero's Solutions for Pollack-Inconsistency
	http://doi.org/10.1007/978-3-319-43144-4_2
	http://www.proof-technologies.com/holzero/hzsyntax_itp2016.pdf


Concerning HOL4 and HOL Zero, I am looking for introductions to them in the 
literature. The appropriate candidates seem to be, at the first glance (without 
having read them already):

	Mark Adams: Introducing HOL Zero (Extended Abstract)
	http://doi.org/10.1007/978-3-642-15582-6_25

	Konrad Slind, Michael Norrish: A Brief Overview of HOL4
	http://doi.org/10.1007/978-3-540-71067-7_6

The latter I found as reference no. 14 of Mark's 2016 paper.

Please let me know if you have other suggestions.


Kind regards,

Ken Kubota

____________________

Ken Kubota
http://doi.org/10.4444/100





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