From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id D6F885D5 for ; Fri, 28 May 2021 06:06:14 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.83,229,1616454000"; d="scan'208,217";a="510382217" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 28 May 2021 08:06:06 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 37258E0B0B; Fri, 28 May 2021 08:06:06 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 7A525E0B0D; Fri, 28 May 2021 08:05:50 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=david.nowak@univ-lille.fr; spf=Pass smtp.mailfrom=david.nowak@univ-lille.fr; spf=None smtp.helo=postmaster@smtp-out-2.univ-lille.fr IronPort-PHdr: =?us-ascii?q?A9a23=3AOgFB+hLfY9WnwVdQ+dmcuHBgWUAX0o4c3iYr45Y?= =?us-ascii?q?qw4hDbr6kt8y7ehCGtLM33AGCANqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j?= =?us-ascii?q?94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd?= =?us-ascii?q?+KvjoFoLIgMm7yuS/94fNbwhLhTexbrN/IRerpgjNq8cahpdvJLwswRXTuHtIf?= =?us-ascii?q?OpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBn?= =?us-ascii?q?MVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0i?= =?us-ascii?q?ScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsZfWDBODY2?= =?us-ascii?q?hbIUBAfQPM+FDoobnu1cOqAGzBQmwCO7tzDJDm3/43bc90+QkCQzI0hYvH8wPs?= =?us-ascii?q?HvJsd77LKASUO6vw6nL0D7OaO5Z1i3j6IjJbx8tu/eMXbV+cMXLykkiDB7FjlO?= =?us-ascii?q?RqYz7Jj+V0uUNs2yf7+V+T+6vhXQnphh3rzOyycgilpPHiZgJylDY6yp52oA1K?= =?us-ascii?q?MW4RkNmfdKqHpRduSGVOodoQc4uXm9ltSQ6x7AFuJO2fjYGxZUjyhLDaPGKfIa?= =?us-ascii?q?F7xbjWuuSJTp1mHxodryhixu290Wr1+PyVs6x0FlQrypFlMHBtnEL1xzJ68iIU?= =?us-ascii?q?OFx/km72TqXygDT7OBEIV4tmarfKp4hxrowmYQOvUjZEC/2gl36jKCXdkU4+ui?= =?us-ascii?q?o9v/obq/6qZ+bMo94kh3xMqMrmsynHes3LBIOX3SB9eS7zr3j8kv0S6hJgP0ui?= =?us-ascii?q?qTVrZTXKMsBqqKnAwJY3Zwv5wuhAzqiytgVnnoKIEpYdB6bi4XlIUzCLfTkAfu?= =?us-ascii?q?lnVihnytny+rJM7DuBJjGM2LNn637fbln7k5R0Aozws5b55JTErwBO/fzWlPpt?= =?us-ascii?q?NDBCR85LhC0z//5BNlny4MeX2OPArGAPKPWsF+I4uYvLPeWaI8bojbxM/kl5/j?= =?us-ascii?q?wgn8lgVIRYK2k0JQNZHymHvlrLF+VbWfyjtoFC2sHvQkzQPTviFKYUD5TY3iyX?= =?us-ascii?q?7g75jE+EI+pEJ3MRp6sgLOcxiu7GJpWZ25cBVCPCnroaoOEW/YSaC6LJs9hkzg?= =?us-ascii?q?EVby/RIM72xGurhf2y6B7IerM5i0YqZXj2cBp6OLJkBEy8SV4D8Cc02GWU2F5h?= =?us-ascii?q?XgIRj8z3KBnu0Nx0FaD0a5ig/xZD9Nf/f1JUh0iP57G0+N6E8zyWh7GftqRVFm?= =?us-ascii?q?mRcymDSgtQdI13t8BeF1wG86ijxDGxyqlGaUZl72NBJwu86LTxWL9J8hnyyWO6?= =?us-ascii?q?K50hF4/B8BLKGeOh6hl9gGVCZSN20yWm6+CcaUHwDWL/2eKyW+DploeSwM0Ga7?= =?us-ascii?q?MWHRaYkrNsfz44FnDRvmgE/BvMgJaysOGLu5BY9PkpVVPX/TuPNCYZHi+3y+oB?= =?us-ascii?q?A7NzbeRZqL3fWQDmSHcDEwJ1Q4JuT6HLgE0CyOlrifDFzF0DnrkZwXn+Ow4oXj?= =?us-ascii?q?9U0xwhwiBaxdJyqax+wUJnrqBV/4D16lCtSs87310G1L43tTYDPKEphF9Z+NHZ?= =?us-ascii?q?s4n61pJ0njWukp7M4DkZ6Rvj1hbbh96pWvh0BJ4DohPi883tGhsxw13beqAzkh?= =?us-ascii?q?pfCicm4vqO/vcLWy2tBWueafMn1/ZysuT0qIO+v0i7Uj8tkekGldk63E0/cNS1?= =?us-ascii?q?i6w74vLAEI0Vo34UQ5j+xFkpr2cZC4i7oD8yHttL+ywszvG1pQnHr12mV6bY95?= =?us-ascii?q?DPfbcR0fJGMoACp3rcbRy87BGRg8CPf4X8K8wO87geeHUgcZD3c57mS6+yGNa/?= =?us-ascii?q?MUnlF+K9jQ5Tu/M25tDzevKhmNvsh/hila/98T2nYRJIz8ITDLX9A=3D=3D?= IronPort-HdrOrdr: =?us-ascii?q?A9a23=3ADtfw5aCZtKgE7trlHenC55DYdb4zR+YMi2TD?= =?us-ascii?q?sHoRdfU1SKKlfqyV9sjztiWatN9yYhodcLm7UcG9qBjnmaKdj7N9AYuf?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AFAADNh7BgfViB/sJaDgsBAQEBAQEBA?= =?us-ascii?q?QEBAQEBAQEBAQESAQEBAQEBAQEBAQEBggYBAQEBAQELAYMhVwE5MYRIiQSIcpt?= =?us-ascii?q?OgWgLAQMBDTEOAgQBAYFcgnSCAAIdBwEEMwYOAgQVAQEFAQEBAgEDAwQBEwEBD?= =?us-ascii?q?xQIQ4VoDYI4KQGEDB0BASYKBwEYDigOAj8hgwMBgwsLi36cCoEygQGCBwEBBoJ?= =?us-ascii?q?VhAmBWQmBOgGHBgGGYCcQgVVEgTwcgikFgklxFwKBJhVSgmo2gi6CF0qBIwETB?= =?us-ascii?q?VlfUAswHJBoQ485iHKRTSwHgWeBM4EmBguIVIcsgyKJNINehjGEaIVmkHaQa4R?= =?us-ascii?q?WiWqCKpJ/GmUBhDY1gQwpgX4zGid2AYI+CTUSGQ6OH4NwgT6DVoUFCD8/ATE4A?= =?us-ascii?q?gYBCQEBAwlYiilbAQE?= X-IPAS-Result: =?us-ascii?q?A0AFAADNh7BgfViB/sJaDgsBAQEBAQEBAQEBAQEBAQEBAQE?= =?us-ascii?q?SAQEBAQEBAQEBAQEBggYBAQEBAQELAYMhVwE5MYRIiQSIcptOgWgLAQMBDTEOA?= =?us-ascii?q?gQBAYFcgnSCAAIdBwEEMwYOAgQVAQEFAQEBAgEDAwQBEwEBDxQIQ4VoDYI4KQG?= =?us-ascii?q?EDB0BASYKBwEYDigOAj8hgwMBgwsLi36cCoEygQGCBwEBBoJVhAmBWQmBOgGHB?= =?us-ascii?q?gGGYCcQgVVEgTwcgikFgklxFwKBJhVSgmo2gi6CF0qBIwETBVlfUAswHJBoQ48?= =?us-ascii?q?5iHKRTSwHgWeBM4EmBguIVIcsgyKJNINehjGEaIVmkHaQa4RWiWqCKpJ/GmUBh?= =?us-ascii?q?DY1gQwpgX4zGid2AYI+CTUSGQ6OH4NwgT6DVoUFCD8/ATE4AgYBCQEBAwlYiil?= =?us-ascii?q?bAQE?= X-IronPort-AV: E=Sophos;i="5.83,229,1616454000"; d="scan'208,217";a="510381929" X-MGA-submission: =?us-ascii?q?MDGtJzyrUw0fdmsctITiBUHIuDHb2bH7D19Vfy?= =?us-ascii?q?gFGNGZqTCHiWbDuD/c35xaEfbVOWwpC8ZKCkzcH5fEPL4NUxXOq0D8Z+?= =?us-ascii?q?AflNrz49PH+aTjYFph3P9icg1KMH6EXB/5ebS+lWzsYbGv6DJZtXdVBB?= =?us-ascii?q?B0HYRZTJEkZDvzxBHVbLYXjw=3D=3D?= Received: from smtp-out-2.univ-lille.fr ([194.254.129.88]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 28 May 2021 08:05:19 +0200 Received: from smtp2.univ-lille.fr (smtp2.univ-lille.fr [10.140.10.73]) by smtp-out-2.univ-lille.fr (Postfix) with ESMTP id 7AF0C160F41; Fri, 28 May 2021 08:05:19 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=univ-lille.fr; s=dkim; t=1622181919; bh=4kmICCH7ZLCqS4qJQ6cJsarmwHrZzbaefFwhlgIFYgQ=; h=From:Subject:Date:Cc:To:From; b=SAHsuco6e6nEvwBlVCz4zaqx/XUJFchqEqaL29nxii+82HsbhJDG9UUZIBN67M5VN MMWfDsHVF9lP86AUTjvmcKYVZ/ZErafQnPXaxccRDL44UtSj3iZewq+7+0bkgfoqwg qBf+qbessZgbKY9dJOIx/22UBmy9n7U96P7v2INNH+920Bxa6BmkYo7cxr1j8AiT3S yEA/+6CNK9RWDqaxMW8WE5FC8U5hE2fj1tOl9Ci9eKDMWeOYCC3usd3KL0SfKPuW48 jLyDlPzpjdz2avL+Q02Vo8FyHX8KHvDkqKT6Xxq5WHlIXCXEKdXEXE1tM6x3HM7xXU N2h0JGgPTgA7g== Received: from smtpclient.apple (44-240-190-109.dsl.ovh.fr [109.190.240.44]) (Authenticated sender: david.nowak@univ-lille.fr) by smtp2.univ-lille.fr (Postfix) with ESMTPSA id 718B53FF91; Fri, 28 May 2021 08:05:18 +0200 (CEST) From: David Nowak Content-Type: multipart/alternative; boundary="Apple-Mail=_A5C8BA48-7E15-4988-AD03-8F2F2F31E7C3" Mime-Version: 1.0 (Mac OS X Mail 14.0 \(3654.80.0.2.43\)) Message-Id: <8D28C8D0-8EFB-4BB0-B62B-227EFA0579DF@univ-lille.fr> Date: Fri, 28 May 2021 08:05:17 +0200 Cc: gilles grimaud , Samuel Hym 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 X-Mailer: Apple Mail (2.3654.80.0.2.43) Subject: [Caml-list] PhD position on program verification in Coq Reply-To: David Nowak X-Loop: caml-list@inria.fr X-Sequence: 18509 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: --Apple-Mail=_A5C8BA48-7E15-4988-AD03-8F2F2F31E7C3 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 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 = =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94 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 = =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94 All the best, --=20 Gilles Grimaud, Samuel Hym, David Nowak --Apple-Mail=_A5C8BA48-7E15-4988-AD03-8F2F2F31E7C3 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
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

=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94
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.

=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94

All the best,

-- 
Gilles Grimaud, Samuel Hym, David = Nowak

= --Apple-Mail=_A5C8BA48-7E15-4988-AD03-8F2F2F31E7C3--