The Coq mailing list

[Aymeric Fromherz <aymeric.fromherz AT inria.fr>]

[Apologies for cross-posting]

Dear all,

We are offering two fixed-term research engineer positions at Inria Paris to develop an integrated
development and verification environment (IDVE) for Rust programs. These posts are part of the
CIRCUS project (https://ptcc.fr/projets/circus-2/), a collaboration between the Prosecco team at
Inria Paris (https://team.inria.fr/prosecco/) and Cryspen (https://cryspen.com/).

Successful applicants will join a team developing the CIRCUS IDVE, consisting of
the hax framework (https://github.com/hacspec/hax) and the Aeneas toolchain
(https://github.com/AeneasVerif/aeneas). Depending on background, missions
might include working on tooling, on extending the hax compiler, on the integration
of proof assistants into the IDVE, and on developing efficient proof methodologies
for reasoning about Rust programs.

Applications and more information online at
Compilation and Tooling Engineer: https://recrutement.inria.fr/public/classic/fr/offres/2023-06892
Proof and Verification Engineer: https://recrutement.inria.fr/public/classic/fr/offres/2023-06891

For more information, please contact me by email (aymeric.fromherz AT inria.fr)

Best,
Aymeric Fromherz,
Prosecco Team, Inria Paris