The Coq mailing list

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

The Prosecco research team at Inria Paris 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; website; tutorial; recent paper; code)

• miTLS*: Attacking and Proving TLS 1.3 Implementations
  (website; code; papers; sample internship topic)

• Efficient Formally Secure Compilers to a Tagged Architecture
  (brief project description, draft paper #1, paper #2, paper #3, code)

• A Verified Browser Security Engine
  (web security models; defensive _javascript_; sample internship topic)

• Dependable Property-Based Testing
  (project description, paper #1, paper #2, draft paper #3, code)

PostDocs (usually on 2 year positions) can also propose and follow their own research agenda and be fairly independent. Researchers (on 3 year or permanent positions 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