Max Kirchmeier (Jul 31 2020 at 14:11): Max Kirchmeier (Jul 31 2020 at 14:11):I'm working on a project that aims to bridge Isabelle and CompCert, i.e. making it possible to extract verified programs from Isabelle in an IL, which can be compiled using the later stages of the CompCert tool-chain.
I'm wondering who to get into contact with to discuss the CompCert side of things. Maybe there are some knowledgeable people here? :)
Yannick Zakowski (Jul 31 2020 at 14:28):That sounds like an interesting project!
There are quite a lot of experts in CompCert nowadays, so it would probably just be a matter of finding one that has the time to discuss this project with you.
I'm not sure there's a clear best entry point for this, but here's a definitely non-exhaustive list of relevant people you may try to contact off the top of my head, hoping it may help.
In France, you have a Parisian cluster arounds Xavier Leroy and Jacques Henri Jourdan among others, another one in Rennes around Sandrine Blazy, David Pichardie and Delphine Demange. David Monniaux in Grenoble as well.
In the US you have all the people at Princeton around the VST project, so Andrew Appel, Lennart Beringer and their collaborators.
In South Korea, Chunk Gil Hur also knows CompCert by heart.
Last updated: Apr 20 2024 at 13:01 UTC