Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Research Programmer in HoTT and Cubical Type T...

view this post on Zulip Email Gateway (Mar 13 2021 at 11:12):

From: Favonia via Cl-isabelle-users <>
We are hiring a research programmer at University of Minnesota to work with
us on building next-generation proof assistant technology (broadly defined)
based on homotopy type theory and cubical type theory. The ideal candidate
would have some knowledge and interest in homotopy and cubical type theory,
combined with concrete experience implementing type theoretic proof
assistants using modern algorithms, such as bidirectional type checking and

You will be exposed to the latest research in the field and can get
involved in theoretical development of the research ideas. We welcome
applicants who do not have a Ph.D. degree---a BA/BS degree is sufficient.

The research project is funded by the AFOSR through their MURI program, and
your official affiliation would be the University of Minnesota with Favonia
being your supervisor. However, you will frequently meet and collaborate
with other researchers from Carnegie Mellon University, Wesleyan
University, University of San Diego, and other institutions. Especially
during the COVID-19 pandemic, most activities will be online, though you
will have to be physically in the US. (We may be able to sponsor visas.
Contact Favonia <> for details.)

We are interviewing candidates on a rolling basis until a match is found.
Candidates applying by the end of March (2021/3/31) would be given priority.

Here is the official link for application: Please also drop an email to Favonia
<> so that we can confirm that your application correctly enters
the system. If you are a current employee of the University of Minnesota,
please use instead.

Some further information

About $60,000 USD.

As soon as you are ready.

The position will last as long as the project can support it and benefit
from it. However, the expectation is that you will be in this position
around 1-3 years (negotiable) and may choose to leave early (for example,
to start a Ph.D.). Your official contract will be one-year but renewable.

This requirement exists to satisfy an administrative requirement of the job
code at the University of Minnesota. We will recognize a wide range of
activities as “work experience”, such as contributions on GitHub during
weekends. Please document related activities in your CV. If you are not
sure if something counts as work experience, please ask Favonia <


Please send an email to Favonia <>.


Last updated: Jan 25 2022 at 01:11 UTC