caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] PhD position on program verification in Coq
@ 2021-05-28  6:05 David Nowak
  0 siblings, 0 replies; only message in thread
From: David Nowak @ 2021-05-28  6:05 UTC (permalink / raw)
  To: coq-club, agda, caml-list, haskell-cafe, pip-club,
	isabelle-users, acl2, hol-info, lean-user, pvs, mizar-forum
  Cc: gilles grimaud, Samuel Hym

[-- Attachment #1: Type: text/plain, Size: 3323 bytes --]

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

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}
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


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


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.


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.


All the best,

Gilles Grimaud, Samuel Hym, David Nowak

[-- Attachment #2: Type: text/html, Size: 6666 bytes --]

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2021-05-28  6:06 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-05-28  6:05 [Caml-list] PhD position on program verification in Coq David Nowak

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).