coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Comparing Coq and K

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Cc: grigore.rosu AT runtimeverification.com
Subject: [Coq-Club] Comparing Coq and K
Date: Mon, 3 Feb 2020 19:26:20 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f51.google.com
Ironport-phdr: 9a23:DLKsihKOpFnsjOWtINmcpTZWNBhigK39O0sv0rFitYgfLvXxwZ3uMQTl6Ol3ixeRBMOHsq4C17Wd6viwESxYuNDd6StEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQZjId4Jas8yBTFrmZUd+lV2GhkIU6fkwvm6sq/4ZJu/T5ct+49+8JFTK73Y7k2QbtEATo8Lms7/tfrtR7NTQuO4nsTTGAbmQdWDgbG8R/3QI7/vjP1ueRh1iaaO9b2Ta0vVjS586hrUh7ohzwZODM/7Wral9Z/jKNfoBKmuhx/34vZa5ybOfZiYq/Qe84RSHFfVchNSSNOHoK8b5MOD+UfO+ZYs5L9rEYKoRenGAWgGP/jxjpOi3Tr36M1zv4hHBnJ0wIgEdwAs2naosvpO6oJTeC50LPFwSnfY/9K2zrw7pXDfBA7ofGLWLJ9adfcxlM0FwjYk1uQsY3lPy+J1usTqWib9PdrWOW0hGI9sQ59uDauyt03ionRh4IV1kzE+jtjwIYuPtC4R0t7bsSlEJtUrS2VK4x2QsY7TmxupS00xLoGuZuhcygLzpQq3wXfa/2Ic4iQ5hLsTuCRLS1/hHJ/d7Kznxmz/lK+yu39SMa0ylJKoTRfktnLtnEBzRvT6tKISvdl40ehwSiA1wbV6u1eP087iLfbJ4Y7wr4tkJoTrUXDHirol0XokqCWbEQk+uap6+v7eLrmup6cN4hyig3kLqsuncm/DOIlOQYNR2iW4fqw2KHn8EHjQ7hHjuc6nrTYvZzHP8gWprO1DglI2Yg58Rm/FS2p0NEAkHkHMl1FfBWHgpDsO17UIfD4Ce6zglSikTt23vzGML3sDojXInjMl7fherl960pCxwYp0d9f4JdUBqkAIPL1REDxqMTVAgElPwGw2erqC9Vw2pkDVW+OH6OVKqPfvUKQ6uIqOeaMZYsVuDjnK/gi4v7jlWQ2lUUHcqWz05obcmu4HuxnI0WFfXrjnM0BEXwRswoxSezlklyCUTpJa3muWKI84yk3CJi6AofbWoCtnLuB0T+nEZ1Rf2BKE0yDEXP1d4qfQPoMcyKTIsp5kjMeT7ShSokh1QuvtADg0bZnIPDUqWUkssfI08E9zOnOn1lm/jttSs+ZzmulTmdun2pOSSVgj45lpkko4F6YmZNgguBEGMZIr6dDFA58KtjH1+1mF93oQSrOe96ITBCtRdDwUmJ5dc4439JbOxU1IN6llB2WmnPyW+ZExYzOP4Q99+fn51a0Is98z3jc06x41gspR8JOMSutgastrlGPVb6MqF2QkuORTYpZxDTErT7Rwm+HvUUeWwl1A/2cACIvI3DOpNG83XvsCr+jDbN9b1lEwM+Gb7pVM5jn0AwAS/DkN9DTJWm2njXoCA==

Dear Grigore,

This blog-post caught some attention from Coq-users, who don't fully
understand how to compare the two systems.

https://runtimeverification.com/blog/k-vs-coq-as-language-verification-frameworks-part-1-of-3/

you later added that K is automatic (not interactive) and faster than Coq.

I'm wondering by what benchmark it is faster than Coq.

Emilio Gallego suggested that K might be a way to address the third
challenge of the poplmark.
"Challenge 3: Testing and Animating with Respect to the Semantics"
https://blog.sigplan.org/2020/01/29/mechanized-proofs-for-pl-past-present-and-future/

However, I've been unable to find solutions of the poplmark in K.

I've found the following solutions to challenge 3 (but the poplmark
website seems down).
https://xavierleroy.org/POPLmark/locally-nameless/
https://www.seas.upenn.edu/~plclub/poplmark/fairbairn.html
https://www.seas.upenn.edu/~plclub/poplmark/berghofer.html
https://www.seas.upenn.edu/~plclub/poplmark/xi.html

Best regards,

Bas

[Coq-Club] Comparing Coq and K, Bas Spitters, 02/03/2020
- Re: [Coq-Club] Comparing Coq and K, Benjamin C. Pierce, 02/03/2020
- Re: [Coq-Club] Comparing Coq and K, Brandon Moore, 02/06/2020
  - Re: [Coq-Club] Comparing Coq and K, Bas Spitters, 02/06/2020