Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] [isabelle] 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] [isabelle] In a world of perfect interoperability between proof assistants, what tools would you combine?


Chronological Thread 
    < Chronological >      < Thread >
  • From: Peter Lammich <lammich AT in.tum.de>
  • To: Talia Ringer <tringer AT cs.washington.edu>, Coq-Club <coq-club AT inria.fr>, isabelle-users <isabelle-users AT cl.cam.ac.uk>
  • Subject: Re: [Coq-Club] [isabelle] In a world of perfect interoperability between proof assistants, what tools would you combine?
  • Date: Mon, 18 May 2020 14:02:20 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lammich AT in.tum.de; spf=Pass smtp.mailfrom=lammich AT in.tum.de; spf=None smtp.helo=postmaster AT mail-out2.informatik.tu-muenchen.de
  • Ironport-phdr: 9a23:U4S66xRmz62LBZm7X5koPhfjDtpsv+yvbD5Q0YIujvd0So/mwa6zYBGN2/xhgRfzUJnB7Loc0qyK6v2mADRdqsve+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLq8UanYtvJqkxxxbLv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/XrJgcJskq1UvBOhpwR+w4HKZoGVKOF+db7Zcd8DWGZNQtpdWylHD4ihbYUAEvABMP5boYfgp1UAsxWwCguiBOzzzTFHiXD40LYm0+kjCwzKwBYtE84MvXnSsd77NL0SUeewzKTQ1zvMce9W1inn6IPVdB4uu/SMXbdxccXNyUkkCgTIjlGKpozgOjOV1/gCs2iA4uphU+KjkXInqxx0ojS128gjlJDEi4QIwV/L6St32pw6JcGkSEFle96kFoNduiKaOYZ4Qs0uXm5mtSg+x7EYtpO3YSoHxZA6yxLCdfGLbYaG7w7+WeuRPTt1hXxrdb2/ihu88EWt1+PyW8mq3FtMsyFLkcHMu2gQ2xHd98SLUOZx80el1DqVywzf8O9JLEEymKHGMZAu2KQwmYAWsUnbHi/5hkH2jKiOe0Uh4Oeo6uDnbqzhpp+BK494lBvyMqUomsyxBuQ4KA0OUHKH+eS9173v51H5QKhTgv0zj6nWrpbaKtgbpqGnBQ9ZyJss5AinAzen1tQXg2UHIUpYdB+JkoTlIUzCLfD8APuln1igijlmyvHeMr3kGJrNL3zDkLn7fbZ67k5R0A4zwspa55JRC7EOPPLzV1TwtNzeFBM5LxG0w+P9BNpgyIwSQXiPDbOBMKPOrV+I4foiLPWLZI8MoTryN/wl5+P1gnIigl8cfayp3YMNZ3yiH/RmJV+ZYXv2jdsbH2cKpFl2cOu/tFSGUDcbXXe0UK8mrmUnEoOgAorZbou2xqOIxye6GJJKYWYAB1yRRzOgXIKdHtwIdSjadsRmi3kPUaWrY44nzxCn8gHgnf4vL/Hd8CAcsZ+mycN4/fabwRAp/DZ5C8CQlnyWQntvtmgMATQ/2eZ2qgpgyQHQ/7J/hqlgGMBe/bttWwI/NJXch7h+AtX3WwnBVtaPDkq7R5OqDGdiHZoK39YSbhMlSJ2ZhRfZ0n/vWudNzu3ZNNkP6qvZmkPJCYN4wnfC2rMmigB/EMpJc3G7g+hz+lqKXtObowCij6+vMJ8k8mvN+WOEljXcuUhZVEt3TLmfG3EZaEzMqN3l50CEU6LrDKkqNABBxMjEJqYYMoS132UDf+/qPZHlW0z0g325XE/ax7XKcJfvPWkQjn3Q
Hi

I would like to see Compcert, at least its backend (IR, optimizations,
machine code generation), being usable from Isabelle.
Then I could probably retarget my Refinement Framework to use Compcert-
IR as a backend, closing the gap from very high-level specifications to
machine code. Similar for CakeML (Currently, the Refinement Framework
targets LLVM or SML).

--
Peter



On Sun, 2020-05-17 at 16:42 -0700, 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