[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
([email protected]).
