From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) 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_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x738.google.com (mail-qk1-x738.google.com [IPv6:2607:f8b0:4864:20::738]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id acf73c5a for ; Tue, 1 Jan 2019 02:12:53 +0000 (UTC) Received: by mail-qk1-x738.google.com with SMTP id r145sf34482552qke.20 for ; Mon, 31 Dec 2018 18:12:53 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1546308772; cv=pass; d=google.com; s=arc-20160816; b=XJ2dv/x1Hp/BYkynDuYntdTb+upuaoRb8omhdB8F2SW2mjWmcga1PwHC1wLTbaXINw 3+jQiNyNEjr7s1BQj7nJpi2YsyWUhI+XbbsKsz7rXbx44lByGJKFkaO0BZU5MiGEGPzB FsiljKHPv9C2mzLxdJ7w63JXRvTkLscAskGLgV366VN6xeJ+/Lo6/BD9O0WwjA6FQaoW fMDT92tq3RtV85+ARaUwMatjQXyIAqNV+WG+7+eD5kuHE9rDJ2dBm7c1f+1KCBu4w89S W5CVnLJVpaHpAGOPe53TrRKuzDtAoB9vgxhYt5xVbsz/uzZlqO/o1ZI+mT/0WUcmjEgI Oipg== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature; bh=UEtnvneswV3pfLRBM3mL83enpsB3Vt/YNd2+Dh7/M1U=; b=zDgurkEoXgfhx1+gW1CK9dD6nfdZKlUM+Qzu3QkoBgMx4TjE4dZbZB718eFHF8rOMG prpKPEECUur6lqF07uluTNUhOUe8sx7o44QCO9oilXmbUDYBinRU2wUogYK/++/H5aTA 8YQTcSJhzRqOGPFMxSAnHw+OdqFzzY7pgCvPiBJ4mhNsZaFe9mxDjg65p8E4f+N/fZ6t pMXm5BEE4geDwUkbgL6wbV6h9vcNNLuHSRmgInwIRdwZpp1wUW8Hglpg7vzfv4s7+Niv jG3jiwzmcNUleczBHVfu3DXKnTny0Er3VvgKbwIrEhaNMC/xo1yJXI/TgJyWB16x1TrR vrXg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=QnKsg4Vs; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=umn.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=UEtnvneswV3pfLRBM3mL83enpsB3Vt/YNd2+Dh7/M1U=; b=I+gp/LoXqsLDafx0VeQLLOPTLKXIa8W0f4N2Uy9bHwZWyVn1ELT2an9IvQpcmpMhCq 1/5Y1ucpRY4Q+u2892FFbewA4qxnI8y+yBU5DzXMXir5Ep+y9EerIen+kHWEFDJV+zoT SoT72Hl2h68fOi8UKKwFITM5StqMiBEN9m/jbRfeny1diG6xtEAAA6JQhC2SeGarI7uJ A2RY2UIMrsQ2xbx9EDBC+s9iXfaNUzO46+1C4wqf8eJ8XD8Qh/FwmUFb39CBx7jnRLmU jULHFjLrMmIepUC2B1LMkd9V9jZHjvkBP0K9Xt4FV53in/ABq68rq3pJ74pZfEppH8o2 UnCw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=UEtnvneswV3pfLRBM3mL83enpsB3Vt/YNd2+Dh7/M1U=; b=C3jmWfrI6EIAumyOvA106ozZ4f0K09qWLshh08vFsyTtpLUrKgP24ReQ5906XkB1dk dtfYk1PRR8QZ5W8kIJffs4pMbNgBfLJ7j3R9+lPyQj+8qD9FmmpjHH/tATgFRJmWgIM8 Ca38mIZqMBYlt8D0e48W2HhO2Y8UE9i0tZF0W8bGFLCh18IkAcSkTP+EkNCbwJKubTZj FfJTNiYwcvWr8p8l1cPlmTYzZmPw58UQ8gQx0Rt3vbwaE2EXSSZHg2QE4CCgaek47evE AxiULp8fK9Udf1GmyqXACEXN8Q7tiMv3qVz8mlJASmECqXFOgu4497PJSu/zxD4LjhIj Mq9g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukd7/5dn/jd8vgCohsXWY8L4vLLIHPNSigQqjtiscuLd88/kBVts 7dpsiDOb0A8UgZXoONjnZiM= X-Google-Smtp-Source: ALg8bN6qP5raHTMG9umP3JKYltE4919TCTH9Zhf4EPFktIwDCkceReufiDZAyohohixJgz8DgjPKnA== X-Received: by 2002:a0c:b59b:: with SMTP id g27mr594450qve.0.1546308772018; Mon, 31 Dec 2018 18:12:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:3133:: with SMTP id g48ls5511031qtb.3.gmail; Mon, 31 Dec 2018 18:12:51 -0800 (PST) X-Received: by 2002:ac8:38fa:: with SMTP id g55mr29418661qtc.10.1546308771767; Mon, 31 Dec 2018 18:12:51 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1546308771; cv=none; d=google.com; s=arc-20160816; b=MsNGFA1onXIsGSA7N0aFUBEK4dBTiqQy75yjJmvpSkTm1zKHUWSj08sej4yRcom7f9 D8k5tHF+caae4qq+EnmT+rE/57sJRmTcUTO0O19MzqXBfH1KSQIrdkXgPg+/knu5Bs1c MJMaK89ju4dtJh97O33/MKrdKY/NJn8jj8pgfn9ZHjeLFo9oSa7wXx6vyDnvgF+oYcAN SMAliIyB7qLwZq/Qt9sCBJvwD9mAAd8hY+XQBr8aHVpBrJZegxhm3xIcNwylWvC404qn hPa5O1gU//5cu89Bwxjroeo92f2cGPuvEPoBkjcUT3MjlpSVf7EYkOANo51orAQQWeDU vHWA== 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; bh=7608CUekZZzxGclVISQk/akQEJkWIpmfoKVUa3O4Q/0=; b=xoMMMeX1k1G+XHzYgLgdoBZ52EwzsjRRBDUskGST3mW7fLidINWN4AOF88kcKMvJ1v o0Tv/ugkUbvgwFP9as6Xftg9uQC3ErrEL0Ru0MsdgjHPioMCGfZjxlKnlr5qR5siy37B 2MLD0uMXuInZfvmS3hi9H4ulCTAT3Vnpw1AFfb40wz1k8reVWJGz6E5qVp+Wt9x5/MLj 4IQw0iTsLaQm78ZMFEZYO29wfBxuIAlQcLfarmv0zxm6jnWbV+fOBMsU0tFR7dzcGrLV r7jA98UhXq3d520uDvOfcPcm4DQ8uc+fJXVWLySTM5jg9+PJs17BoHqX92z3YSPpy60y hyFA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=QnKsg4Vs; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=umn.edu Received: from mta-p6.oit.umn.edu (mta-p6.oit.umn.edu. [134.84.196.206]) by gmr-mx.google.com with ESMTPS id j62si1581988qtb.0.2018.12.31.18.12.51 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 31 Dec 2018 18:12:51 -0800 (PST) Received-SPF: pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) client-ip=134.84.196.206; Received: from localhost (unknown [127.0.0.1]) by mta-p6.oit.umn.edu (Postfix) with ESMTP id 1731FBAC for ; Tue, 1 Jan 2019 02:12:51 +0000 (UTC) X-Virus-Scanned: amavisd-new at umn.edu Received: from mta-p6.oit.umn.edu ([127.0.0.1]) by localhost (mta-p6.oit.umn.edu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id c8ZovRh3qOV9 for ; Mon, 31 Dec 2018 20:12:50 -0600 (CST) Received: from mail-lj1-f198.google.com (mail-lj1-f198.google.com [209.85.208.198]) (using TLSv1.2 with cipher AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mta-p6.oit.umn.edu (Postfix) with ESMTPS id A038995D for ; Mon, 31 Dec 2018 20:12:50 -0600 (CST) Received: by mail-lj1-f198.google.com with SMTP id f5-v6so8243157ljj.17 for ; Mon, 31 Dec 2018 18:12:50 -0800 (PST) X-Received: by 2002:a2e:97d7:: with SMTP id m23-v6mr24649143ljj.18.1546308769163; Mon, 31 Dec 2018 18:12:49 -0800 (PST) X-Received: by 2002:a2e:97d7:: with SMTP id m23-v6mr24649135ljj.18.1546308768814; Mon, 31 Dec 2018 18:12:48 -0800 (PST) MIME-Version: 1.0 From: Favonia Date: Mon, 31 Dec 2018 20:12:47 -0600 Message-ID: Subject: [HoTT] Postdoc Position at the University of Minnesota To: types-announce@lists.seas.upenn.edu, agda@lists.chalmers.se, coq-club@inria.fr, ProofTheory@lists.bath.ac.uk, univalent-mathematics@googlegroups.com, homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000e0ed71057e5c1091" 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=QnKsg4Vs; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=umn.edu 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: , --000000000000e0ed71057e5c1091 Content-Type: text/plain; charset="UTF-8" Dear All, I am looking for postdocs for my group at the University of Minnesota, Twin Cities, USA. The length is about 18-24 months but negotiable. The funding can support a wide range of topics in type theory and programming language theory. I am particularly interested in raising the rigor of computer programs or mathematical proofs. To name a few possible research directions: 1. higher-dimensional type theory (e.g., cubical type theory) 2. mechanization of proofs (e.g., in homotopy theory) 3. property-based testing I am open to other topics not on the list. Please check my website https://favonia.org for the work I did. Teaching is not required, but we can discuss it if you are interested. The start date is flexible though I prefer early spring. REQUIREMENT You must have a Ph.D. in Computer Science, Mathematics, Philosophy, or some related field when the job starts. I need your CV, your cover letter (explaining your motivation) and two professional references. PREFERENCE Background in type theory or programming language theory, good publication record, and experience in proof mechanization are all pluses. HOW TO APPLY If you are currently an employee of the University of Minnesota, use this link: https://hr.myu.umn.edu/jobs/int/328079 Otherwise, this is for everyone else: https://hr.myu.umn.edu/jobs/ext/328079 DIVERSITY We take diversity and inclusiveness seriously, which is an important reason why I joined the University. I strongly encourage people of often underrepresented groups (not just regarding race or gender) to consider this position. Best, Favonia they/them/theirs http://favonia.org -- 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. For more options, visit https://groups.google.com/d/optout. --000000000000e0ed71057e5c1091 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear All,

I am looking for postdocs for my group at= the University of Minnesota, Twin Cities, USA. The length is about 18-24 m= onths but negotiable. The funding can support a wide range of topics in typ= e theory and programming language theory. I am particularly interested in r= aising the rigor of computer programs or mathematical proofs. To name a few= possible research directions:

1. higher-dimensional type theory (e.= g., cubical type theory)
2. mechanization of proofs (e.g., in homotopy t= heory)
3. property-based testing

I am open to other topics not on= the list. Please check my website https://= favonia.org for the work I did. Teaching is not required, but we can di= scuss it if you are interested. The start date is flexible though I prefer = early spring.

REQUIREMENT

You must have a Ph.D. in Computer S= cience, Mathematics, Philosophy, or some related field when the job starts.= I need your CV, your cover letter (explaining your motivation) and two pro= fessional references.

PREFERENCE

Background in type theory or= programming language theory, good publication record, and experience in pr= oof mechanization are all pluses.

HOW TO APPLY

If you are cur= rently an employee of the University of Minnesota, use this link:

https://hr.myu.umn.edu/job= s/int/328079

Otherwise, this is for everyone else:

https://hr.myu.umn.edu/jobs/ex= t/328079

DIVERSITY

We take diversity and inclusiveness se= riously, which is an important reason why I joined the University. I strong= ly encourage people of often underrepresented groups (not just regarding ra= ce or gender) to consider this position.

Best,
Favonia
they/th= em/theirs
http://favonia.org

--
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.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000e0ed71057e5c1091--