[TYPES/announce] PostDoc positions at Inria Paris on F* and on Formally Secure Compilation

[Catalin Hritcu]

Hello everyone,

2 PostDoc positions are available in my group at Inria Paris on the
F* and ERC SECOMP projects. I am seeking exceptional candidates
with a strong, internationally competitive research track record.

On F* (https://www.fstar-lang.org/), I am looking for someone with
research expertise in: programming language semantics, dependent
types, type theory, effects, monads, mechanized metatheory, functional
programming, formal verification. Here is a (non-exhaustive) list of
potential research topics on which we could work:
http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2018/fstar-topics.pdf

On ERC SECOMP (https://secure-compilation.github.io/), I am
particularly looking for someone with expertise in:
- formal verification in a proof assistant like Coq
  and verified compilation in particular
- security foundations, e.g., reference monitoring,
  hyperproperties, noninterference
Here is a (non-exhaustive) list of potential research topics:
http://prosecco.gforge.inria.fr/personal/hritcu/temp/habil/catalin_habil.pdf#page=80

Candidates are expected to work collaboratively on project-relevant
topics and help advise students, but can also dedicate some of their
time to their own independent projects. For exceptional candidates
with enough experience we can also discuss about Starting Researcher
positions, who can propose and follow their own research agenda and be
fairly independent. Our team can also support such exceptional
candidates for permanent Researcher positions funded and awarded
competitively by Inria. Further details about these various positions
are available at https://secure-compilation.github.io/#positions

Do not hesitate to contact me if you are interested in joining the team!

Kind Regards,
Catalin