Hi Bill, >Why are miz3 and Mizar the only proof assistants where >one can easily write up human readable proofs?
I'm surprised you're not including Isar in this list! And do you know about ForTheL (see <http://nevidal.org/download/forthel.pdf>)? Now _there's_ a readable formal language! :-) Also, does anyone know what is the status of Mohan Ganesalingam's work in this direction (see for example <http://people.pwf.cam.ac.uk/mg262/CSLI%20talk.pdf>)? Freek ------------------------------------------------------------------------------ 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
