[TYPES/announce] PhD position: Unifying Correctness for Communicating Software

[Jorge A. Perez]

[Please share widely with potential candidates; apologies for any
cross-postings.]

PHD POSITION ON "UNIFYING CORRECTNESS FOR COMMUNICATING SOFTWARE"
University of Groningen, The Netherlands
Deadline: Tuesday, July 31, 2018.
Contact: Dr. Jorge A. Pérez (j.a.perez at rug.nl)

This four-year PhD position is embedded in the project "Unifying
Correctness for Communicating Software", a 5-year VIDI career grant
awarded to Dr. Jorge A. Pérez by the NWO (Netherlands Organization for
Scientific Research).

The project will deliver a comprehensive description of how different
verification techniques for message-passing concurrency relate to each
other.
We will use the Curry-Howard correspondence for concurrency (aka
"propositions as sessions") as a reference in formalizing these
relations.
These foundational results will be validated through case studies and
tool prototypes.


The PhD student will contribute to rigorously compare and systematize
different type systems for message-passing programs (such as session
types).
These comparisons will then be used to streamline existing type
systems for message-passing programs, but also to define new type
systems, following the logical foundations defined by the Curry-Howard
correspondence for concurrency.
The research plan for the PhD student can be shaped depending on
his/her strengths and interests.

The PhD student will join a vibrant research group (three PhD students
and a postdoc), supported by generous research funds.
In particular, he or she will work in coordination with a postdoc
researcher (also to be funded by the VIDI career grant), and will have
the chance of visiting international research collaborators to be
involved in the project.


We look for a talented and dedicated student with an MSc degree (or
equivalent) in Computer Science, Logic, or Mathematics, excellent
communication skills in English, and enthusiastic to work in a team.

Candidates with experience in one or more of the following are
especially encouraged to apply:
- semantics of programming languages and/or program verification
- the Curry-Howard isomorphism (aka "propositions as types")
- concurrency theory and/or process calculi
- modal/substructural logics and (their) proof theory

To apply, please send an email to Jorge A. Pérez (j.a.perez at rug.nl), including:
- a full curriculum vitae;
- a cover letter explaining your motivation to join the project;
- contact information of two references.

Applications received by
Tuesday, July 31, 2018
will receive full consideration; early expressions of interest are encouraged.
The position will remain open until filled; the stating date is flexible.

Further information on the project:
http://www.jperez.nl/vidi

Informal inquiries:
Dr. Jorge A. Pérez (j.a.perez at rug.nl)

-- 
Jorge A. Pérez
Assistant Professor
Bernoulli Institute for Math, CS and AI
University of Groningen, The Netherlands
URL: http://www.jperez.nl