caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: David Nowak <david.nowak@univ-lille.fr>
To: coq-club@inria.fr, agda@lists.chalmers.se, caml-list@inria.fr,
	haskell-cafe@haskell.org, pip-club@univ-lille.fr,
	isabelle-users@cl.cam.ac.uk, acl2@utlists.utexas.edu,
	hol-info@lists.sourceforge.net, lean-user@googlegroups.com,
	pvs@csl.sri.com, mizar-forum@mizar.uwb.edu.pl
Cc: gilles grimaud <Gilles.Grimaud@univ-lille.fr>,
	Samuel Hym <samuel.hym@univ-lille.fr>
Subject: [Caml-list] PhD position on program verification in Coq
Date: Fri, 28 May 2021 08:05:17 +0200	[thread overview]
Message-ID: <8D28C8D0-8EFB-4BB0-B62B-227EFA0579DF@univ-lille.fr> (raw)

[-- 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
(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


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

                 reply	other threads:[~2021-05-28  6:06 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=8D28C8D0-8EFB-4BB0-B62B-227EFA0579DF@univ-lille.fr \
    --to=david.nowak@univ-lille.fr \
    --cc=Gilles.Grimaud@univ-lille.fr \
    --cc=acl2@utlists.utexas.edu \
    --cc=agda@lists.chalmers.se \
    --cc=caml-list@inria.fr \
    --cc=coq-club@inria.fr \
    --cc=haskell-cafe@haskell.org \
    --cc=hol-info@lists.sourceforge.net \
    --cc=isabelle-users@cl.cam.ac.uk \
    --cc=lean-user@googlegroups.com \
    --cc=mizar-forum@mizar.uwb.edu.pl \
    --cc=pip-club@univ-lille.fr \
    --cc=pvs@csl.sri.com \
    --cc=samuel.hym@univ-lille.fr \
    --subject='Re: [Caml-list] PhD position on program verification in Coq' \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

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).