From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,HTML_MESSAGE,LOTS_OF_MONEY,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_KAM_HTML_FONT_INVALID autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 438 invoked from network); 13 Mar 2021 01:15:42 -0000 Received: from mail-ot1-x33d.google.com (2607:f8b0:4864:20::33d) by inbox.vuxu.org with ESMTPUTF8; 13 Mar 2021 01:15:42 -0000 Received: by mail-ot1-x33d.google.com with SMTP id e2sf11537754otk.8 for ; Fri, 12 Mar 2021 17:15:42 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615598138; cv=pass; d=google.com; s=arc-20160816; b=xGlERYFjT2mGYR12Ce7DAdMXolpN1oMRTLxRAf4MWrDbnwHgKBuL7+i1D4FTPqD6+T swJm8QmgPJaEFLbUPuJbe8o3Y5SfrvlAvaX13Yck1mbGN1JJ1sT/l43XDdHRenSqhFbI DhOYryz8d2zCLNlELlzfkkUQdb1V8+DSTb8KashqJ8czib7t/699ctA2WrAtiD9d3gRN PTybP5i3BeFVvd8YyZpnECHUvgJekVY+S8Mt2JMAdbkdATlNi8iMeFRmsc2KeSkPjmIC UANMEqRjDd/LmvID1kumfFOXkMOTV42+8qXyPQV+uvE/aVFBzd+iaDENb311VG86zxrl xx5w== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:reply-to:to:subject:message-id:date:from :mime-version:dkim-filter:dmarc-filter:dkim-signature; bh=VplRhM0xfPdfTsSQBZhU65hv2fq8M3nLyppb+yhrh8c=; b=U6nrZ0OLB803KP9hdYKFhLYmIoUI33kxBfRXLhm5d49O88eO3pNdQl9ipm31IKg5Vk X2hRMOGz+0IquDOtcNvONrSVAfMxXAWpgXyUn9qGZHHgLLTkuE/AkUh1jJMuhX5OXaHn mNYVd40Q3ufv1A+SBsli/u4+kIEspaKDWq/7D0pAHz1ryji2wQ43fmZQYRNDViD7PI4L uD6Mz7u9H3zdUsORqAcqfoRu21+AdUlBNMBcgOrr3uZcxJTVtBE8ptYhm+n9saiC2z8O CCzdhJvWOUOt9+syd8nhkxGM6Q9KujDt4AqfQT8rEqh+pjrvMrJ8+ynAfuAy0tP6b6IF aflQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=qVjfWO7b; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.207 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=umn.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=dmarc-filter:dkim-filter:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=VplRhM0xfPdfTsSQBZhU65hv2fq8M3nLyppb+yhrh8c=; b=ik3+RIgUIleqAN6lDFXG/9mI3tWjt5W1ax1PHBf5DnapiSvpXrk1v6G3O3MrdWn4uf LdVe6vJDL9IlICzwaHBZg5uCnM/Y/vjZaQyoh8tJ4cRFGt1BXX3B8cJvGDVTv7VyfzNL ZmYO0w+0D/4kQzsE/WxiEw9eEHeJDClTECtUTwYOGZ6wUbHZ8O+SrbfjId1TYhJnifGv 7qsnv68G8hhTEnieLenBlFmCIIYLmYbRnmbVB4dYIqOSNg5aO2TcXvoGNhpAqf2lAz+P KQUhg+L9iV/56Ao5fxQskHCNgKSqMEf4tGOocCtvq7I0p0LJLH0BAsfuAR6xhK+nd57L EOrw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:dmarc-filter:dkim-filter:mime-version:from:date :message-id:subject:to:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=VplRhM0xfPdfTsSQBZhU65hv2fq8M3nLyppb+yhrh8c=; b=uOAq6oWYQPZrswklIhuFjkIGgL3Tzeq+Gr/ybM70+Lv+lbuu6fcNTB8MAnylpas9ex kt4cA6fvZfRWV/4JVxiA/TFYgssdZq3IilLhUlr7LrfB6H3RCvlZ8PGXubztgbQ9r8n2 JIPMi9SmGTBAfLn4vQMh4Vs4wloRT5c/Y7db8Ko6izOxpz5fKU8Db1xM9r27ky1FAMg1 xMJEx1p4cYFuA/Tt0oLZfAD811ryzRhO218DhHI+ST5+OHlyowTphuXkTwpsynG/EZMh 7SNoD/j7ZbVA7l4j8NNf5J9VlCYzajwC6fDz3yO714l44PcAn+GTYcW7vNDlkNeRpj/B Dpdg== X-Gm-Message-State: AOAM533NlPcxlrsUMih2oMoVdPE0YCjz9dU8JZjZA2qJBbloHkFm4xYS kjiCQkEuRkuAOe6e8G2Nrdk= X-Google-Smtp-Source: ABdhPJwKFAg7dQk+RSWM7gZDcWzM/FY9yImzhsKztBjoD+H8iqOipmsHnYOBWP3IK5JOHOGYgZKjCw== X-Received: by 2002:aca:4e8e:: with SMTP id c136mr11808400oib.97.1615598137959; Fri, 12 Mar 2021 17:15:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:1156:: with SMTP id u22ls2578739oiu.6.gmail; Fri, 12 Mar 2021 17:15:37 -0800 (PST) X-Received: by 2002:aca:530c:: with SMTP id h12mr11564560oib.172.1615598137471; Fri, 12 Mar 2021 17:15:37 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615598137; cv=none; d=google.com; s=arc-20160816; b=bXJvgfks/CcaQzJr+81IfxwfhUhLkANJtSs/k8+Ut23wjMPuIzLn1m3HZI15d7Z19z 3si6QPdyKb82/dq4ky7JOGy2UMoIdlxF8Y5/zFNyCt7wlFc+B3c5Jh/U7aPz3YLXIr2W MBPXg2aS1gN0OBIIVI4fFWXqNqq6aFSv1NSBYh8T6XbXGGzGRf1JJZL0tKLIOhuyMUvz T9jU5WcXBo2HM98SUEZh8DWZIVn11b4wpH0n1JZ7Z8/aG9PsnT2v+KwicM6lY1syMq7b 1kJzOdE5DqxriwqH/YIPeo7CiSpVXeZo9Aeg4nLzs5QgPvqmDyy4BpyeFR0IKFnIBZe+ pIEA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :dkim-filter:dmarc-filter; bh=DsFwibwsdWGEhozmSE6MLCzY0D1h3SIa2ehpG2hht28=; b=SsvtEc6CH/wm/ZISsU3lNrS0V19uKzjK/KJT6yI7tZdA3TKxK8d+PbURQFnqCSuyg2 zFfK1nT3yZzBmIqOaz+QvpgB+2XdS/jzTY199GsdsU3ob3btX6K4BLoPvUOQ0x1O5szs 7GIWT0SSW/hcu/YE6kzo3VSrtQ4A+YFJRd2d+0No4HGjsz9w90YXPcjvT3y93Iy+dLCe YhipMklmKiSP2kLJIQDM2teNg35W/mc1pGc1jgw6+O0BZo4ei9EnWW+C7FPevLoalQ53 azeFtaCaPg5VdBt4QqSi9AqdLdENFW+OUnFgxw9h3iEs7zTkYczyCGhbAHVgZChp9BYN 5lPg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=qVjfWO7b; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.207 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=umn.edu Received: from mta-p7.oit.umn.edu (mta-p7.oit.umn.edu. [134.84.196.207]) by gmr-mx.google.com with ESMTPS id f2si86121oob.2.2021.03.12.17.15.37 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 12 Mar 2021 17:15:37 -0800 (PST) Received-SPF: pass (google.com: domain of kbh@umn.edu designates 134.84.196.207 as permitted sender) client-ip=134.84.196.207; Received: from localhost (unknown [127.0.0.1]) by mta-p7.oit.umn.edu (Postfix) with ESMTP id 4Dy4Vw6q1Xz9vKSh for ; Sat, 13 Mar 2021 01:15:36 +0000 (UTC) X-Virus-Scanned: amavisd-new at umn.edu Received: from mta-p7.oit.umn.edu ([127.0.0.1]) by localhost (mta-p7.oit.umn.edu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id Ctg6PEmWiZKP for ; Fri, 12 Mar 2021 19:15:36 -0600 (CST) Received: from mail-yb1-f198.google.com (mail-yb1-f198.google.com [209.85.219.198]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mta-p7.oit.umn.edu (Postfix) with ESMTPS id 4Dy4Vw3wJbz9vKSd for ; Fri, 12 Mar 2021 19:15:36 -0600 (CST) DMARC-Filter: OpenDMARC Filter v1.3.2 mta-p7.oit.umn.edu 4Dy4Vw3wJbz9vKSd DKIM-Filter: OpenDKIM Filter v2.11.0 mta-p7.oit.umn.edu 4Dy4Vw3wJbz9vKSd Received: by mail-yb1-f198.google.com with SMTP id l3so31344801ybf.17 for ; Fri, 12 Mar 2021 17:15:36 -0800 (PST) X-Received: by 2002:a05:6902:1003:: with SMTP id w3mr23082095ybt.445.1615598135981; Fri, 12 Mar 2021 17:15:35 -0800 (PST) X-Received: by 2002:a05:6902:1003:: with SMTP id w3mr23082079ybt.445.1615598135782; Fri, 12 Mar 2021 17:15:35 -0800 (PST) MIME-Version: 1.0 From: "'Favonia' via Homotopy Type Theory" Date: Fri, 12 Mar 2021 19:14:59 -0600 Message-ID: Subject: [HoTT] Research Programmer in HoTT and Cubical Type Theory To: types-announce@lists.seas.upenn.edu, agda@lists.chalmers.se, coq-club@inria.fr, ProofTheory@lists.bath.ac.uk, univalent-mathematics@googlegroups.com, Homotopy Type Theory , cl-isabelle-users@lists.cam.ac.uk Content-Type: multipart/alternative; boundary="000000000000fbc0ea05bd60c0ac" X-Original-Sender: kbh@umn.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=qVjfWO7b; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.207 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=umn.edu X-Original-From: Favonia Reply-To: Favonia Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000fbc0ea05bd60c0ac Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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 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=E2=80=99s a =E2=80=9Cwork experience=E2=80=9D requiremen= t. What counts as =E2=80=9Cwork experience=E2=80=9D? 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 =E2=80=9Cwork experience=E2=80=9D, such as contributions on G= itHub during weekends. **Please document related activities in your CV.** If you are not sure if something counts as work experience, please ask Favonia . - I have more questions! Please send an email to Favonia . Best, Favonia they/them/theirs --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAH_%2Brvc0nayUNeSQvprodnpdQTfuXSLHeEicWTddRUhFRSDSxA%40= mail.gmail.com. --000000000000fbc0ea05bd60c0ac Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

We are hiring a research programmer at University of = Minnesota to work with us on building next-generation proof assistant techn= ology (broadly defined) based on homotopy type theory and cubical type theo= ry. The ideal candidate would have some knowledge and interest in homotopy = and cubical type theory, combined with concrete experience implementing typ= e 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 resear= ch ideas. We welcome applicants who do not have a Ph.D. degree---a BA/BS de= gree 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 Fav= onia being your supervisor. However, you will frequently meet and collabora= te with other researchers from Carnegie Mellon University, Wesleyan Univers= ity, 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@u= mn.edu> for detai= ls.)


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

<= br>

Here is the official link fo= r application: https://hr.myu.umn.edu/jobs/ext/339220<= span style=3D"font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-= color:transparent;font-weight:400;font-style:normal;font-variant:normal;tex= t-decoration:none;vertical-align:baseline"> Please also drop an email to Fa= vonia <= kbh@umn.edu> so t= hat we can confirm that your application correctly enters the system. If yo= u 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.<= /span>


- How long does t= his position last?

Th= e 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=E2=80=99= s a =E2=80=9Cwork experience=E2=80=9D requirement. What counts as =E2=80=9C= work experience=E2=80=9D?

This requirement exists to satisfy an administrative requirement of th= e job code at the University of Minnesota. We will recognize a wide range o= f activities as =E2=80=9Cwork experience=E2=80=9D, 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 Fav= onia <k= bh@umn.edu>.


- I have more questio= ns!

Please send an em= ail to Favonia <kbh@umn.edu= >.=C2=A0


Best,
Favonia
they/them/theirs<= br>

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAH_%2Brvc0nayUNeSQvprodnpdQTfu= XSLHeEicWTddRUhFRSDSxA%40mail.gmail.com.
--000000000000fbc0ea05bd60c0ac--