Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?


Chronological Thread 
    < Chronological >      < Thread >
  • From: Heiko Becker <hbecker AT mpi-sws.org>
  • To: coq-club AT inria.fr, Talia Ringer <tringer AT cs.washington.edu>, isabelle-users <isabelle-users AT cl.cam.ac.uk>
  • Subject: Re: [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?
  • Date: Fri, 29 May 2020 08:29:31 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=hbecker AT mpi-sws.org; spf=Pass smtp.mailfrom=hbecker AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:xdwLXROlX8ql3rDxIyEl6mtUPXoX/o7sNwtQ0KIMzox0I/T4rarrMEGX3/hxlliBBdydt6sZzbOM7OuwByQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagYb5+Ngi6oRvTu8UZgoZvK7s6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyocKTU37H/YhdBxjKJDoRKuuRp/w5LPYIqIMPZyZ77Rcc8GSWZEWMtaSi5PDZ6mb4YXEuQPI+hYoYn+qVUAoxSxCgujC//gxDJTmn/737c33/g9HQzI3gEtGc8FvnTOrNXyMacfSeK7w7fJzTXAaPNdxCrw55bUfRAiv/6MR697fM3RyUY0CQzKklaQppL/Pz6O0+QNq2mb4/N7VeOhkG4rsQZxoiKgxso1jITCm40axEze+ypj3IY1OcO3SFR9YdO8DJdcqiWXOpZqTs0iTW9mtiQ3x7wCtJKnfSUHzIoryh7fZvGGfIWF4wzvWeeVLDtmh39oZryxigqy/0W9yODyVs+520tEoCpCl9nDrHEN1xrL58iCUvt9/16t2S2B1gDI8O1EJlo0laXdJpU8wbAwjoIevVnNEyLygkn6kaubel8n9+Wp8ejrf7XrqoeYOoNpkA3zM6YjltaiDeglMAUCRXWX9fi62bb+50P2Wq9KgeczkqTBsJDVO8AbpqmhDg9Xz4Yj8xe/Dyu439QCh3UHKUpFeBOeg4jqP1HOO+v3Ae26g1S0nzdn3e3JMaP5DpXMKHjMjqvhcK5g50NSzAc/181T6pZOBrwCIf//QFL9udzAAh88KQO0wuLnCNtn1oMZXGKCGq+ZP7jMvlCU5eIgPfOMaZQQuDblKvgp/uXujHEimVMHeqmpx5QXZGiiHvt6O0WZfWbsgtAZHGgWuQo+VfXmh0GGUT5OfHm/RLk85zE+CIK+F4jPXIGtgLqb3Ce6BJJafG5GCkrfWUvvIo6DQrIHbD+YCs5niD0NE7a7D8cd3BWvvUfAyrxoI/CcrjECtJTs2cJd7PaVihgp9T1yANia1SeAQ3wi2isJXDY80aR7rAlg0VqZyuAsgudRH9FX4/4MTxw3L4X0xOg8ANn3HAvKOMqKHgWIWNKjVBE8T9E2i/UDaEVwAZ32jhrO1CmnGZcQj73OH4MvtKXG0C6idI5G13/a2fx53BEdScxVODjj3/YnrlSBN8vyi0yc0p2SW+EExieUrzWG1WvLp15DFglqXvedBC1NVg7ttd38o3j6YfquBLAgaFYTy9OaK7dHcJvslVQDR/P4MpLbe233l2riXU/ZlIPJV5LjfiAm5AuYDUEFlw4J+nPfblo7HibkuH3FSjt0GgC2bg==
Hi Talia,

I hope I am not too late to add my answer.

We have a Coq and HOL4 codebase for our floating-point roundoff error checker FloVer [1]. However, the Coq and HOL4 versions have diverged quite a bit now where the Coq version has features that are not present in the HOL4 version, and vice versa.

So I guess in a world of perfect interoperability I would love to be able to transport the formalizations, or at least results checked by the tool, from one theorem prover into the other.

Cheers,

Heiko

--------

[1]: https://gitlab.mpi-sws.org/AVA/FloVer

On 5/18/20 1:42 AM, Talia Ringer wrote:
Say we one day are able to just take things from Isabelle/HOL and use them with Coq developments with no additional effort, or similarly in the opposite direction, or similarly for any other pair of proof assistants. Say we would get strong guarantees about these combined verified systems. Just humor this for a second.

In such a world, what systems would you want to combine, and why?

Talia


Archive powered by MHonArc 2.6.19+.

Top of Page