Dear all,

We have an opening for a 3-year PhD position at University of Lille,
France. The successful applicant will be funded -- including salary
and (international) conference travel -- through a new French-German
ANR-funded project. There will also be an opportunity to collaborate
with a research team in Japan.

Lille is at the heart of Europe: 45 minutes from Bruxelles, 1 hour
from Paris, 1 hour and half from London. This is an important
university hub that hosts the annual International Cybersecurity Forum
(FIC).

The start date is September 1st, but might possibly be postponed to
October 1st.

The PhD position is about the formal proof in Coq for shallow-embedded
imperative programs and their compilation into C (more details below).

Interested students should meet the following requirements:

- Be interested by the topic of the PhD :-)

- Have or be about to complete a Master in Computer Science or a
  related field (Logic, Mathematics, etc.).

If you are interested in applying for this opportunity please begin by
contacting us {gilles.grimaud,samuel.hym,david.nowak}@univ-lille.fr
as soon as possible with the following information:

- CV/Resume

- A brief introduction of yourself, your scientific interests, and if
  you are familiar with any of the following topics:
  * formal proof / formal verification,
  * functional programming
  * monads
  * semantics

———————————————————————————————————
Summary:

The topic of this PhD offer is the formal proof in Coq for
shallow-embedded imperative programs and their compilation into C.
More precisely, the objective is to conceive and develop formal tools
to simplify code writing and proof of system software for low-end
devices.

Context:

The Coq proof assistant [1] allows to prove properties of programs.
Its language, called Gallina, is purely functional. In the Pip project [2],
we have considered a monadic subset of C-like Gallina enough to
formally write an OS kernel.

Objectives:

A first objective of this PhD is to extend the monadic subset in order
to include further imperative features (such as loops, references or
exceptions) that will simplify code writing and proof of system
software for low-end devices. For security properties the monadic
Hoare logic used for Pip will have to be extended to deal with the new
imperative features. For functional properties, there are two possible
directions: either use the monadic Hoare logic or monadic equational
reasoning as developed in Monae [3]. The relation with FreeSpec [4]
should also be investigated.

A second objective is to automatically translate programs written in
this monadic subset into an AST of the CompCert C verified compiler
[5] and to prove formally that this translation is correct, in the
sense that properties proved on the monadic subset are also true of
the generated C code.

[1] https://coq.inria.fr
[2] http://pip.univ-lille1.fr
[3] https://github.com/affeldt-aist/monae
[4] https://github.com/lthms/FreeSpec
[5] https://compcert.org
———————————————————————————————————

All the best,

-- 
Gilles Grimaud, Samuel Hym, David Nowak