From: Kaustuv Chaudhuri <kaustuv.chaudhuri@inria.fr>
To: caml-list@inria.fr
Subject: [Caml-list] Junior engineer position at INRIA Saclay/Ecole Polytechnique, France
Date: Mon, 20 Jun 2011 21:48:00 +0200 [thread overview]
Message-ID: <BANLkTi=XJMJEGNTdUGcs6Yix2hgmfquY6fxvsmh+aM8rnEZrJA@mail.gmail.com> (raw)
The Parsifal research team at INRIA Saclay and the Ecole Polytechnique
has an open call for one junior engineer position (2 years).
The main task of the recruited engineer will be to work on the
integration and further development of a number of computational
logic systems designed and built by the team members in recent
years. Some tasks involved are:
- Designing and implementing a common formal framework for
communication between the Abella proof assistant, the Bedwyr
symbolic model checker, and the Tac inductive theorem prover.
- Using the Teyjus implementation of the Lambda Prolog programming
language to represent and animate logical specifications of
deductive and computational systems.
- Investigating a number of application domains including the formal
meta-theory of computational systems (programming languages,
process calculi, etc.), and the use of formal proofs as
certificates (eg. proof-carrying code, marketplace of proofs).
Candidates should have a bachelor's degree in computer science, be
familiar with the OCaml programming language (or similar high-level
programming languages), and have a background in logic, formal
methods, and symbolic computing.
As this engineer will work with a team of international researchers,
the candidate should be fluent in English. Knowledge of French is
desirable but not mandatory.
The position should begin in October 2011.
Interested candidates are encouraged to contact the following people:
Dale Miller <dale.miller@inria.fr>.
Kaustuv Chaudhuri <kaustuv.chaudhuri@inria.fr>
Some links:
Official announcements:
http://www.lix.polytechnique.fr/parsifal/dokuwiki/doku.php?id=engineer
http://en.inria.fr/institute/recruitment/offers/young-graduate-engineers
Parsifal team web page: http://www.lix.polytechnique.fr/parsifal/
System descriptions:
Bedwyr http://slimmer.gforge.inria.fr/bedwyr/
Abella http://abella.cs.umn.edu/
Tac http://slimmer.gforge.inria.fr/tac/
Teyjus http://teyjus.cs.umn.edu/
reply other threads:[~2011-06-20 19:48 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='BANLkTi=XJMJEGNTdUGcs6Yix2hgmfquY6fxvsmh+aM8rnEZrJA@mail.gmail.com' \
--to=kaustuv.chaudhuri@inria.fr \
--cc=caml-list@inria.fr \
/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