Logic & Programming

My PhD student Wendlasida Ouedraogo defended his PhD thesis on Source code optimization for safety critical software at the École Polytechnique in Palaiseau.

He showed how to do provably correct transformations of source-code for a fragment of the Ada language, used in real-world critical software, inside the Coq proof assistant. Using such transformations, one can optimize programs at the entry of a compiler, and does not pose the burden on proving simulation theorems between various compiler intermediate languages, like it is usually done (ex. in CompCert).

He also developed a tool-chain to write provably correct lexers, CoqLex, lexing previously being a compiling phase that was not done formally.

Congratulations and the best of luck to Wendlasida!

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net