The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

A Postdoctoral Researcher position is available on my secure
compilation project at Inria Paris. The project is aimed at building
the first formally secure compilation chains for realistic programming
languages like C. Such compiler chains will ensure that high-level
abstractions cannot be violated even when interacting with untrusted
low-level code or when some of the program components were compromised.

I am seeking exceptional candidates with a strong, internationally
competitive track record of research in programming languages, formal
verification, or security. Particularly interesting areas include:

- formal verification in a proof assistant like Coq and
  verified compilation in particular

- security foundations, e.g., reference monitoring, hyperproperties,
  noninterference, fully abstract translations

Candidates are expected to work collaboratively and help advise students.

Please see the project web page (https://secure-compilation.github.io)
for more details about the project and about such open positions.
Do not hesitate to contact me if you are interested in joining the team!

Best Regards,
Catalin Hritcu