Skip to Content.
Sympa Menu

coq-club - [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

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


Chronological Thread 
    < Chronological >      < Thread >
  • From: Talia Ringer <tringer AT cs.washington.edu>
  • To: Coq-Club <coq-club AT inria.fr>, isabelle-users <isabelle-users AT cl.cam.ac.uk>
  • Subject: [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?
  • Date: Sun, 17 May 2020 16:42:23 -0700
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wr1-f45.google.com
  • Ironport-phdr: 9a23:jS+pmRGn+r3+EaYKX0yqoZ1GYnF86YWxBRYc798ds5kLTJ7zoM2wAkXT6L1XgUPTWs2DsrQY0reQ6vi8EjZaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmssAndqsYbjYR8Jqov1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2hqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4TzuUEBrR+/BQa2Gejh1j5Ihnn53aIkyeQqDAbL3BA6H9IPtnTUo8v6NL0JXO+p16nE1zvCYOlN2Tf96YjIdB8hoe2LXbJ2a8be11QgFx7cg1iWtIfqMC+b2P4XvGiH8+pvS/ivi2g/pgx+vjSiwskhhIbHiIwbzl3I6Tt1zZspKNO3VUJ2ZcOpHptNuyyVKYZ7Td8vTm9ntSs4xLALuJ22cTUXxJklxhPSbeGMfYuQ4h/7SuqdPTN1iGhmdb+/nRq+71asxvDmWsS70FtHqDdOnMPWuXAXzRPT79CKSvtj8Uel3jaCzwXT5ftFIUAwjKbaJYQhzqMpmpodvknOHjX6mErxjK+ReUUk/van5/77bbXho5+QL450igfgPaQygsGzH/g0PwwUU2WY+emwzqPv8VPkTLlQgfA7krHVsJXAKsQaoq65DRVV0oEm6xunEzemytUYnX8ILF1bYhKKlJTmO0rULPH2F/i/mFSskDZtx/DJIr3hBZPNImLdn7j8YLZx81RcxxYrzdBD+5JUDakML+70Wk/ordDXEhs5MxGvzOv8E9V81oYeWXqVDaODMaPSt0WI5uM1LOWWao8VomW1F/9wzPn3yFQ9hFVVKaKuxN4cbG2yNvVgOUSQJ3T21JNJEHwDtAc6SOGvlUaPSyUbM3epVqgx4jU2TZ+9AJ3YboupxreI2WGyFdtLZTYVJEqLFCLUfoGFUr82aSSdL9UpxiAeVL6uRpUJ3groqwbhy7thIfbT/GsVuY+1h4s93PHaiRxnrW88NM+ayWzYFzgozFNNfCc/2eVEmWI40k2KiPkqiOceCtVI5/JPXRs9M9jRw/EoU4mvCDKERc+ATROdevvjATw1SYhskdoHYkI4BM/7yx6fgmylBLgak7HND5sxoPqFjirBYv1lwnOD75EPylwvQ89BL2qj3/8t/BOVGIfSk0SfmLqtc+IR0DOfrWo=
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