Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] In a world of perfect interoperability between...

Email Gateway (Aug 23 2022 at 09:10):

From: Talia Ringer <tringer@cs.washington.edu>
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

Email Gateway (Aug 23 2022 at 09:11):

From: Peter Lammich <lammich@in.tum.de>
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).

Last updated: Apr 25 2024 at 04:18 UTC