Re: [Hol-info] How to find existing developments in HOL4?

2017-09-11 Thread Mario Castelán Castro
Thanks Chun and Ramana. On 11/09/17 06:26, Chun Tian (binghe) wrote: > Well .. I didn’t reply to the mailing list because it contains some insulting > words to third-party products. But since you forwarded it already, I’m fine > with that. Oops. I am sorry for that. > I didn’t know you were lo

Re: [Hol-info] How to find existing developments in HOL4?

2017-09-11 Thread Mario Castelán Castro
Thanks you very much. On 10/09/17 23:18, john.harri...@cl.cam.ac.uk wrote: > Hi Mario, > > | If you know of an existing formalization of elementary topology in HOL4 > | please let me know, so that I can avoid duplicating work. > > Not in HOL4, but in HOL Light there is quite a bit of topology, w

Re: [Hol-info] How to find existing developments in HOL4?

2017-09-11 Thread Ramana Kumar
I think a good approach is to ask the mailing list (as you have done), and to look around in the src and examples directories of the repository. On 11 September 2017 at 12:26, Chun Tian (binghe) wrote: > Well .. I didn’t reply to the mailing list because it contains some > insulting words to thi

Re: [Hol-info] How to find existing developments in HOL4?

2017-09-11 Thread Chun Tian (binghe)
Well .. I didn’t reply to the mailing list because it contains some insulting words to third-party products. But since you forwarded it already, I’m fine with that. I didn’t know you were looking for formalizations of pure mathematics theories, but here is my another little experience: 1. Go t

[Hol-info] SOAP@SAC 2018, April 9-13, Pau, France - (EXTENDED DEADLINE) final call for papers

2017-09-11 Thread sac . soap2018
(Apologies for duplicates) FINAL CALL FOR PAPERS - SOAP track at SAC Service-Oriented Architectures and Programming track of the 33st ACM/SIGAPP Symposium On Applied Computing 9-13 April 2018, Pau, France http://sac-soap.sdu.dk/soap2018/ IMPORTANT DATES September 25 (EXTENDED), 2017: S