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

[Jorge A. Perez]

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

This PhD position was already advertised earlier this month.
The text below includes some important updates (in particular, a link
to an official application form).
Apply before August 24. Early expressions of interest are encouraged.

Best regards,
Jorge A. Pérez


============
PHD POSITION ON "UNIFYING CORRECTNESS FOR COMMUNICATING SOFTWARE"
University of Groningen, The Netherlands
Apply before August 24, 2018, following the link given below.
Contact: Dr. Jorge A. Pérez (j.a.perez at rug.nl)
Further information: http://www.jperez.nl/vidi


* Job Description

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 various
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 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 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.


* Qualifications

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


* Application

You may apply for this position until 23 August 23:59h / before 24
August 2018 Dutch local time.

Please use the application form in the following university website:
https://www.rug.nl/about-us/work-with-us/job-opportunities/overview?details=00347-02S0006JQP

Please upload your complete application in English as a single PDF-file.
The submission should contain the following:
1. A full curriculum vitae
2. A cover letter explaining your motivation to join the project
3. Contact information of two references.


* Conditions of Employment

The University of Groningen offers a salary of € 2,266 gross per month
in the first year up to a maximum of € 2,897 gross per month in the
fourth year.
It is a temporary assignment for a period of four years. First, you
will get a temporary position of one year with the perspective of
prolongation with another three years. Before the end of the first
year, there will be an evaluation as to the feasibility of successful
completion of the PhD thesis within the next three years.

The University of Groningen has adopted an active policy to increase
the number of female scientists across all disciplines of the
University.
Therefore, female candidates are especially encouraged to apply.

The preferred starting date is 1 October 2018.


* Additional Information

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

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