Thus, it may be reasonable to conclude that I have now successfully built HOL Light.
Excellent, Colin! Yeah, if you're not getting strange bugs, you should conclude this. > What are you using HOL Light in order to do? I'd like to code up an early auction theory result due to Vickrey as a worked example for a PhD workshop I'm giving next month. Sounds really cool! Feel free to explain to us how proof assistants are going to help out with Economics. So you're the chairman of the Mathematical Finance Department of Economics University of Birmingham? I downloaded your paper http://www.springerlink.com/content/e47110g182480115/fulltext.pdf from your web page http://www.socscistaff.bham.ac.uk/rowat/ It looks interesting. How does Theorema compare to HOL Light? This grabbed me: Arrow’s theorem in social choice has attracted the most attention, including studies by Wiedijk [18] using Mizar, Nipkow [15] using HOL, and Grandi and Endriss [6] using Prover9. Noncooperative game theory has also received attention, including by Vestergaard and co-authors [16] with Coq. -- Best, Bill ------------------------------------------------------------------------------ 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
