Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: Bruno Barras <bruno.barras@inria.fr>
To: caml-list@inria.fr, coq-club@inria.fr, agda@lists.chalmers.se,
	 types@lists.chalmers.se
Subject: [Caml-list] Coq-related postdoc position at Inria-Saclay
Date: Mon, 02 Sep 2013 13:30:46 +0200	[thread overview]
Message-ID: <522476E6.5010509@inria.fr> (raw)


The Paral-ITP Project (French ANR funding) is looking for candidates
for a 1 year post-doc position, to begin as soon as possible, at
Inria-Saclay, France.

* Position description:

The Paral-ITP Project aims at exploiting the potential of multi-core
processors to improve the user interaction with highly trustable
interactive proof assistants. See the Paral-ITP website for more
information (link below).

The position is focused on the implementation of a distributed kernel
for the Coq proof assistant which would feature the verification of
independent proof-checking tasks concurrently.

* Context :

The successful candidate will work under the supervision of Bruno
Barras and collaborate with Enrico Tassi on the Ecole Polytechnique
campus. He will also have contacts with other teams of the Paral-ITP
Project, namely Fortesse (LRI, Orsay) and Pi.r2 (Inria, Paris).

* Requirements:

Candidates should have a Ph.D. in Computer Science (or give evidence
that the defense is planned soon). They should also be familiar with a
proof assistant in type theory (preferably Coq, Agda or Matita) and be
experienced in the development in a functional programming language
(ML, Haskell). The expertise in concurrency paradigms and the ability
to produce high quality code will be important criteria.

* Application:

Applicants should send an email to Bruno Barras (bruno.barras@inria.fr)
including a CV, a list of publications, and a short (two pages at
most) statement about their research activities. It may also include
the names of up to 2 references.

The deadline for applications is September 15, 2013. Notifications of
acceptance or rejection will be sent out no later than September 30.

* Links:

http://paral-itp.lri.fr/
http://www.inria.fr/centre/saclay


                 reply	other threads:[~2013-09-02 11:30 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=522476E6.5010509@inria.fr \
    --to=bruno.barras@inria.fr \
    --cc=agda@lists.chalmers.se \
    --cc=caml-list@inria.fr \
    --cc=coq-club@inria.fr \
    --cc=types@lists.chalmers.se \
    /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
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox