[Hol-info] CFP: 2018 IEEE/ACM Design Automation Conference Hardware Design Contest

The 2018 IEEE/ACM Design Automation Conference Hardware Design Contest features embedded hardware implementation of neural network based target tracking for drones. Contestants will receive training dataset provided by our industry sponsor DJI , and a hidden dataset will be us

Re: [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light?

On 01/09/17 15:12, Ken Kubota wrote: > Hi Mario, > > John has explained some of his motivation for HOL Light in an email > available online at […] Thanks you. These links provide useful insight. > A HOL family tree with both HOL4 and HOL Light can be found at […] and at […]. Yes, I have read th

Re: [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light?

My highly subjective opinions: as an end-user, I choose HOL4 over HOL light because I think and/or found: 1. Standard ML is a better language than OCaml (as a programming language); 2. Poly/ML is a better implementation than OCaml (as a language implementation); 3. HOL4 has a richer and more syst

Re: [Hol-info] HOL Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light?

On 02/09/17 18:05, Chun Tian (binghe) wrote: > My highly subjective opinions: as an end-user, I choose HOL4 over HOL light > because I think and/or found: > > 1. Standard ML is a better language than OCaml (as a programming language); > 2. Poly/ML is a better implementation than OCaml (as a langu