Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Research Programmer in HoTT and Cubical Type Theory
@ 2021-03-13  1:14 'Favonia' via Homotopy Type Theory
  0 siblings, 0 replies; only message in thread
From: 'Favonia' via Homotopy Type Theory @ 2021-03-13  1:14 UTC (permalink / raw)
  To: types-announce, agda, coq-club, ProofTheory,
	univalent-mathematics, Homotopy Type Theory, cl-isabelle-users

[-- Attachment #1: Type: text/plain, Size: 3254 bytes --]

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
normalization-by-evaluation.

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 <kbh@umn.edu> 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:
https://hr.myu.umn.edu/jobs/ext/339220 Please also drop an email to Favonia
<kbh@umn.edu> 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 https://hr.myu.umn.edu/jobs/int/339220 instead.

# Some further information

- What is the annual salary?

About $60,000 USD.

- When is the expected start date?

As soon as you are ready.

- How long does this position last?

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.

- I see that there’s a “work experience” requirement. What counts as “work
experience”?

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 <kbh@umn.edu
>.

- I have more questions!

Please send an email to Favonia <kbh@umn.edu>.

Best,
Favonia
they/them/theirs

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH_%2Brvc0nayUNeSQvprodnpdQTfuXSLHeEicWTddRUhFRSDSxA%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 11177 bytes --]

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2021-03-13  1:15 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-03-13  1:14 [HoTT] Research Programmer in HoTT and Cubical Type Theory 'Favonia' via Homotopy Type Theory

Discussion of Homotopy Type Theory and Univalent Foundations

This inbox may be cloned and mirrored by anyone:

	git clone --mirror http://inbox.vuxu.org/hott

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V1 hott hott/ http://inbox.vuxu.org/hott \
		homotopytypetheory@googlegroups.com
	public-inbox-index hott

Example config snippet for mirrors.
Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git