Email Gateway (Feb 09 2024 at 23:09): Email Gateway (Feb 09 2024 at 23:09):From: Jim Grundy <jim.grundy@acm.org>
I thought folks on the list would like to know that my team at AWS is working on a few projects using interactive theorem provers. We use Lean and HOL Light, but our largest effort at the moment uses Isabelle/HOL. You can find me on jmgruj@amazon.com if you would like to connect directly.
Regards
Jim Grundy
https://www.linkedin.com/in/jim-grundy-b050b21/
Email Gateway (Feb 09 2024 at 23:31):From: Peter Lammich <lammich@in.tum.de>
Dear Jim
Is "you are working on something with Isabelle" all information that is
publicly available, or can you give more details?
Regards
Peter Lammich
Email Gateway (Feb 10 2024 at 00:37):From: Jim Grundy <jim.grundy@acm.org>
With respect to the Isabelle/HOL work specifically, for now I can say publicly only that we’re reasoning about Rust code. I will follow later when I can say more.
Regards
Jim
Last updated: Jan 04 2025 at 20:18 UTC