On Thu, Aug 23, 2012 at 5:26 AM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> Thanks! But the OP (me) really was asking a different question: why
> aren't you, Konrad, Rob and Michael all working on the same program, which
> you could maybe call HOL4LightPower? Wouldn't that increase productivity?
> John, you seem to be on the extreme Math end of CS, and I like that a lot,
> but Konrad, Rob and Michael are making a real good impression on me as
> well. I think I'm missing something about fundamental programming
> incompatibilities, or different aims. Rob said that HOL Light is about
> proving theorems (which is why I use it, I think), and HOL4 was about
> hardware and software verification.
My slides from the last ITP conference are somewhat relevant:
http://xrchz.net/sozi.svg. Hopefully not impossibly cryptic without a
speaker.
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
