U tweetove putem weba ili aplikacija drugih proizvođača možete dodati podatke o lokaciji, kao što su grad ili točna lokacija. Povijest lokacija tweetova uvijek možete izbrisati. Saznajte više
BTW, several colleagues asked what is the difference between K and Coq. I refer interested people to this blog: https://runtimeverification.com/blog/k-vs-coq-as-language-verification-frameworks-part-1-of-3/ … In short, K gives fast executability and automation, while Coq gives more proof interactivity. Wish I had time to cover that in my talk.
So, K seems closer to boogie and why3 than to @CoqLang
By what benchmark is it faster than Coq?
How does K perform on the poplmark?https://blog.sigplan.org/2020/01/29/mechanized-proofs-for-pl-past-present-and-future/ …
Hi Bas, sorry for my late reply. I only check Twitter once a week. I believe K is closer to Coq than why3 or boogie, because it is a framework, backed by a language independent logic, where languages are theories (and not translations to a core). Let's continue via email.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.
