[TYPES/announce] Positions for students and young researchers at Inria Paris in Prosecco team

[Catalin Hritcu]

The Prosecco research team <http://prosecco.gforge.inria.fr/> at Inria Paris
<https://www.inria.fr/en/centre/paris-rocquencourt> is looking for
excellent, highly motivated students and young researchers for research
internships and PhD, PostDoc, Research Engineer, or Researcher positions.
We have external funding for a couple of PhD and PostDoc positions we can
fill over several years with significant flexibility and can also support
strong candidates for Researcher positions funded and awarded competitively
by Inria.

Prosecco does formal and practical security research on cryptographic
protocols, web security, and hardware security mechanisms. To this end, we
design and implement programming languages, formal verification tools,
dynamic monitors, testing frameworks, verified compilers, etc. Our current
projects include:

   -

   F*: From Program Verification System to Proof Assistant
   (hot topics
   <http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2016/fstar.pdf>;
   website <https://www.fstar-lang.org/>; tutorial
   <https://www.fstar-lang.org/tutorial>; recent paper
   <https://www.fstar-lang.org/papers/mumon/>; code
   <https://github.com/FStarLang/FStar>)
   -

   miTLS*: Attacking and Proving TLS 1.3 Implementations
   (website <http://mitls.org/>; code <https://github.com/mitls>; papers
   <http://www.mitls.org/wsgi/publications>; sample internship topic
   <http://prosecco.gforge.inria.fr/personal/karthik/teaching/mpri-mitls.pdf>
   )
   -

   Efficient Formally Secure Compilers to a Tagged Architecture
   (brief project description
   <http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2016/secomp.pdf>,
   draft paper #1 <http://arxiv.org/abs/1510.00697>, paper #2
   <http://prosecco.gforge.inria.fr/personal/hritcu/publications/micro-policies.pdf>,
   paper #3 <http://ic.ese.upenn.edu/abstracts/sdmp_asplos2015.html>, code
   <https://github.com/micro-policies>)
   -

   A Verified Browser Security Engine
   (web security models <http://prosecco.gforge.inria.fr/webspi/>; defensive
   JavaScript <http://www.defensivejs.com/>; sample internship topic
   <http://prosecco.gforge.inria.fr/personal/karthik/teaching/mpri-browser-core.pdf>
   )
   -

   Dependable Property-Based Testing
   (project description
   <http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2016/quick-chick.pdf>,
   paper #1 <http://arxiv.org/abs/1409.0393>, paper #2
   <https://hal.inria.fr/hal-01162898/document>, draft paper #3
   <https://www.cis.upenn.edu/~llamp/pdf/Luck.pdf>, code
   <https://github.com/QuickChick>)

PostDocs (usually on 2 year positions) can also propose and follow their
own research agenda and be fairly independent. Researchers (on 3 year
<https://www.inria.fr/en/institute/recruitment/offers/starting-research-positions/presentation>
or permanent positions
<https://www.inria.fr/en/institute/recruitment/offers/young-graduate-scientist/competitive-selection>
via a competitive Inria national contest) are expected to be highly
independent. The research internships are for students at any level (BSc,
MSc, and PhD) and usually take between 3 and 6 months. The predominant
language of communication in Prosecco is English.

If you are interested in applying or have any questions please send us an
email at karthikeyan.bhargavan at inria.fr and catalin.hritcu at gmail.com.

Happy holidays, Karthik and Catalin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20151222/6ecb8421/attachment-0001.html>