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