Gagallium

In 2011, I designed a formally verified C parser for my master's internship. You can refer to our ESOP paper (with François Pottier and Xavier Leroy) to see the details. Here, I am going to explain what problems (and some of their solutions) I have to overcome in order to use it in Compcert, the certified compiler developed at Gallium in Coq.

Tuesday October 16 is an excellent day for a lot of truly excellent reasons. The one of concern here is that it was chosen to be the Ada Lovelace Day, whose purpose is to celebrate important women in one’s scientific field.