<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div class=""><div class="">Dear all,</div><div class=""><br class=""></div><div class="">We have an opening for a 3-year PhD position at University of Lille,</div><div class="">France. The successful applicant will be funded -- including salary</div><div class="">and (international) conference travel -- through a new French-German</div><div class="">ANR-funded project. There will also be an opportunity to collaborate</div><div class="">with a research team in Japan.</div><div class=""><br class=""></div><div class="">Lille is at the heart of Europe: 45 minutes from Bruxelles, 1 hour</div><div class="">from Paris, 1 hour and half from London. This is an important</div><div class="">university hub that hosts the annual International Cybersecurity Forum</div><div class="">(FIC).</div><div class=""><br class=""></div><div class="">The start date is September 1st, but might possibly be postponed to</div><div class="">October 1st.</div><div class=""><br class=""></div><div class="">The PhD position is about the formal proof in Coq for shallow-embedded</div><div class="">imperative programs and their compilation into C (more details below).</div><div class=""><br class=""></div><div class="">Interested students should meet the following requirements:</div><div class=""><br class=""></div><div class="">- Be interested by the topic of the PhD :-)</div><div class=""><br class=""></div><div class="">- Have or be about to complete a Master in Computer Science or a</div><div class=""> related field (Logic, Mathematics, etc.).</div><div class=""><br class=""></div><div class="">If you are interested in applying for this opportunity please begin by</div><div class="">contacting us {gilles.grimaud,samuel.hym,<a href="mailto:david.nowak}@univ-lille.fr" class="">david.nowak}@univ-lille.fr</a></div><div class="">as soon as possible with the following information:</div><div class=""><br class=""></div><div class=""><div class="">- CV/Resume</div></div><div class=""><br class=""></div><div class="">- A brief introduction of yourself, your scientific interests, and if</div><div class=""> you are familiar with any of the following topics:</div><div class=""> * formal proof / formal verification,</div><div class=""> * functional programming</div><div class=""> * monads</div><div class=""> * semantics</div><div class=""><br class=""></div><div class="">———————————————————————————————————</div><div class=""><div class="">Summary:</div><div class=""><br class=""></div><div class="">The topic of this PhD offer is the formal proof in Coq for</div><div class="">shallow-embedded imperative programs and their compilation into C.</div><div class="">More precisely, the objective is to conceive and develop formal tools</div><div class="">to simplify code writing and proof of system software for low-end</div><div class="">devices.</div><div class=""><br class=""></div><div class="">Context:</div><div class=""><br class=""></div><div class="">The Coq proof assistant [1] allows to prove properties of programs.</div><div class="">Its language, called Gallina, is purely functional. In the Pip project [2],</div><div class="">we have considered a monadic subset of C-like Gallina enough to</div><div class="">formally write an OS kernel.</div><div class=""><br class=""></div><div class="">Objectives:</div><div class=""><br class=""></div><div class="">A first objective of this PhD is to extend the monadic subset in order</div><div class="">to include further imperative features (such as loops, references or</div><div class="">exceptions) that will simplify code writing and proof of system</div><div class="">software for low-end devices. For security properties the monadic</div><div class="">Hoare logic used for Pip will have to be extended to deal with the new</div><div class="">imperative features. For functional properties, there are two possible</div><div class="">directions: either use the monadic Hoare logic or monadic equational</div><div class="">reasoning as developed in Monae [3]. The relation with FreeSpec [4]</div><div class="">should also be investigated.</div><div class=""><br class=""></div><div class="">A second objective is to automatically translate programs written in</div><div class="">this monadic subset into an AST of the CompCert C verified compiler</div><div class="">[5] and to prove formally that this translation is correct, in the</div><div class="">sense that properties proved on the monadic subset are also true of</div><div class="">the generated C code.</div><div class=""><br class=""></div><div class="">[1] <a href="https://coq.inria.fr" class="">https://coq.inria.fr</a></div><div class="">[2] <a href="http://pip.univ-lille1.fr" class="">http://pip.univ-lille1.fr</a></div><div class="">[3] <a href="https://github.com/affeldt-aist/monae" class="">https://github.com/affeldt-aist/monae</a></div><div class="">[4] <a href="https://github.com/lthms/FreeSpec" class="">https://github.com/lthms/FreeSpec</a></div></div><div class=""><div class="">[5] <a href="https://compcert.org" class="">https://compcert.org</a></div></div><div class="">———————————————————————————————————</div><div class=""><br class=""></div><div class="">All the best,</div><div class=""><br class=""></div><div class=""><div dir="auto" class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">-- <br class="">Gilles Grimaud, Samuel Hym, David Nowak</div><div dir="auto" class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><br class=""></div></div></div></body></html>