On 5/08/12 5:18 PM, Bill Richter wrote: > Thanks, Ramana! I've often wanted Isabelle locales. Are you going to > code them in HOL4? For readability I'd like to not "constantly have > this annoying TarskiModel hypothesis hanging around," as Michael > said, but it would be good to write up a longer version of at least > part of my code to show that I can avoid both new_axiom and > new_type.
Coding up something like locales is a big project, as the Isabelle developers would confirm (having been refining the design and implementation of theirs for over a decade). As work that is unlikely to lead to much direct academic benefit, it's difficult to motivate spending the time on it. There is a simple locale-like thing in HOL4, which was implemented by Bruno Barras, who wanted something like Coq's "section" mechanism (itself locale-like) when he visited Cambridge and worked on HOL4 for a spell. The code still works, but was only used for Bruno's one example. No-one else has ever tried to use it, so far as I know, and it's not documented. Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
