[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 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