The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

The Programming Languages group at Delft University of Technology is 
looking for:

- One PhD student (4 years)
- One post-doc (1 year)

The topic of research, which will be determined based on the common 
interests of the candidate and the supervisor, will be in the 
development of expressive program logics for:

- Verification of multilingual software
- Verification of asynchronous I/O
- Verification of non-functional properties (time/space/security 
properties/...)
- Verified compilation

This work will revolve around Iris <https://iris-project.org/>: a 
higher-order concurrency separation logic framework that is implemented 
in the Coq proof assistant <https://coq.inria.fr/>. Iris has been 
successfully used for a variety of applications including but not 
limited to logical-relations for relational reasoning, program logics 
for relaxed memory models, program logics for object capabilities, and a 
safety proof for a realistic subset of the Rust programming language.

The successful candidates will work under the supervision of Robbert 
Krebbers <https://robbertkrebbers.nl> and Eelco Visser 
<https://eelcovisser.org/>.

# Requirements for the PhD position

- A master's degree (or equivalent) in computer science, with a strong 
interest in program verification, proof assistants, and program semantics.
- A strong commitment to research.
- Previous experience with Coq or separation logic is preferred, but not 
necessary.

# Requirements for the post-doc position

- A PhD degree in computer science, in a topic related to program 
verification, proof assistants, and program semantics.
- A strong publication record.
- Previous experience with Coq and separation logic.
- Previous experience with Iris is preferred, but not necessary.

# Application instructions

More information about the vacancies and information how to apply can be 
found at:

- PhD student: 
https://vacature.beta.tudelft.nl/vacaturesite/permalink/50824/?lang=en
- Postdoc: 
https://vacature.beta.tudelft.nl/vacaturesite/permalink/50825/?lang=en

The starting date of both positions will be decided with the candidate 
(earlier dates are preferred).

Informal inquiries to Robbert Krebbers <mail AT robbertkrebbers.nl> are 
welcome.