UNSOUND workshop at SPLASH 2024

Stream: Program verification

[Marco Servetto]

Dear Lean community,
I'm one of the organizer of UNSOUND https://2024.splashcon.org/home/unsound-2024.
We would like to host a discussion about the differences between Lean, Coq, Agda and other verifiers, and on what makes the kernel of the verifier less likely to "accidentally" support proofs of false :-)
Would anyone be interested in discussing about this topic?

[Mario Carneiro]

@Marco Servetto This topic is of great interest to me, but I probably can't attend in person. Are you allowing remote participation?

[Marco Servetto]

Hi, Yes, while we do have some in person contributions, most of the contributions will be remote. We are just a small emerging workshop :-)
If you want to have a fast zoom call, we can discuss any details.