Hi Cris, The Common HOL Platform is my attempt at a basis for enabling easy interchange of proofs and source code between HOL systems. It consists of a very precisely defined ML API and an equivalent for HOL theory. I'm afraid I haven't yet produced a coherent document describing it yet (although I have a collection of files that capture it for my personal use). However HOL Zero does conform to the platform, and from version 0.5.0 onwards has an ML module interface for the Common HOL API (commonhol.mli). The behaviour of each ML binding in HOL Zero's ML user interface (which in fact consists of little more than this API) is described in the user manual A-appendices (however these are only 50% complete). Of course the behaviour can also be determined by examining the source code, but this is hardly satisfactory for people. I plan to finish the user manual later this year hopefully.
The platform actually predates HOL Zero by about two years. Part of the motivation for building HOL Zero was producing a clear example of the platform. Mark. on 12/7/12 2:48 AM, Cris Perdue <[email protected]> wrote: > Hello Mark and All, > > I noticed Mark's publication "Introducing HOL Zero", and the abstract > mentions a Common HOL Platform. Can anyone point me to a definition of this? > > Thanks, > Cris ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
