[TYPES/announce] Funded postdoc and PhD positions in theorem proving and intuitionistic mathematics

[Liron Cohen]

We are looking for excellent PhD candidates and postdocs to join our project on “Extending and Applying Implemented Intuitionistic Mathematics”, which is a joint project between Cornell University in the US and Ben-Gurion University in Israel.

The aim of the project is to develop a proof assistant that fully integrates intuitionistic principles, such as the notion of choice sequences, and use the unique resulting computational setting to explore the intuitionistic theory’s wider implications, especially with respect to the broader notion of computation. This implementation includes providing computational interpretations of intuitionistic principles and developing semantics to support them, and using these principles to develop novel intuitionistic theories, namely, intuitionistic calculus and intuitionistic homotopy theory. Another goal is to use the framework to improve the capabilities of theorem proving tools and facilitate significant advances in the internal verification of complex systems.

We invite applications for *funded PhD and postdoc positions* in the field of theorem proving and intuitionistic mathematics. Successful candidates are expected to advance the state of the art of existing theorem provers by resizing the predominant role of type theory in theorem proving especially with intuitionistic mathematics, and producing a more user-friendly alternative setting closer to common mathematical thinking.

Depending on background and interests of the candidates, possible research foci are: implementing intuitionistic principles into a proof assistant; developing an intuitionistic calculus and studying its computational benefits; developing intuitionistic homotopy theory; applying the intuitionistic framework in formal verification.

Successful candidates are likely to have efficient communication skills in English, as well as a track record of research expertise in a subset of the following topics:

* Type inference and type theory
* Intuitionistic or constructive foundations  
* Use of dependent type theories and proof assistants (eg, Coq or Agda)
* Categorical semantics 
* Formal verification

The positions are available immediately, start dates are flexible. Both positions include reimbursement for travel expenses to conferences and there is no teaching load.  

The funds for the PhD position are available for 4 years. The funds for the postdoc position are available for two years in the first instance with the possibility of extension.

This collaborative project will afford excellent candidates the unique opportunity to study with two groups: in Israel (Ben-Gurion University) and the US (Cornell University). A successful candidate would take up the position at Ben-Gurion University in Israel and will also spend parts of their time at Cornell University in the US. The US visits can be very flexible, and travel expenses will be paid for. 

The complete application consists of the following documents, which should be sent as a single PDF file to the email address given below:

* CV (including list of publications)
* One-page cover letter (indicating available start date, relevant qualifications, experience, and motivation)
* Up to three letters of recommendation
* University certificates and transcripts (BSc, MSc, and PhD degrees, if applicable)

Informal inquiries are welcome and should be directed to Dr. Liron Cohen (cliron at cs.bgu.ac.il).