Thanks, Tom!
I have now added a passage on John's historical survey including Thomas Hales'
proof and formalization project (pp. 3 f.) involving also HOL Zero, and a
reference to John's "HOL Done Right" draft:
http://dx.doi.org/10.4444/100.111
In the "Criticism" section, a quote on the limitations of current HOL systems
from John Harrison/Urban/Wiedijk and the attempts to remedy the situation
[Melham, 1993b; Völker, 2007; Homeier, 2009] is added. Thanks to John for
providing the links to his interesting articles.
Then some quotes on why PVS admits only a very restricted form of type
dependency are given, which Natarajan Shankar very kindly explained in an
e-mail:
http://pvs.csl.sri.com/mail-archive/pvs-help/msg01865.html
Ken
____________________
Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100
> Am 01.11.2016 um 18:09 schrieb Thomas Melham <thomas.mel...@balliol.ox.ac.uk>:
>
> I don't think they differ much at all.
> Tom
>
>> On 1 Nov 2016, at 12:20, Ken Kubota <m...@kenkubota.de> wrote:
>>
>> Also, maybe Tom could comment on whether his 1992 article significantly
>> differs
>> from his 1993 article available online at
------------------------------------------------------------------------------
Developer Access Program for Intel Xeon Phi Processors
Access to Intel Xeon Phi processor-based developer platforms.
With one year of Intel Parallel Studio XE.
Training and support from Colfax.
Order your platform today. http://sdm.link/xeonphi
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
