Unfortunately, and embarrassingly, there is not yet a system description paper for HOL Zero. I plan to write one soon (but I think I said that a few years ago..).
I should take a good look at R0 some time and could then comment on it, but good to hear that steps have been taken to address concerns about pretty printing. Clearly the qualities enumerated in Freek's paper are all desirable, but remember that there is also "faithfulness", which isn't fully addressed by the concept of Pollack-consistency. You could print something wrongly but also parse it back in correspondingly wrongly (so, for example, print & parse "true" as "false" and vice versa). Mark. On 13/02/2017 15:38, Ken Kubota wrote: > 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 ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
