From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.161.10 with SMTP id b10mr4442103pgf.21.1511147582675; Sun, 19 Nov 2017 19:13:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.98.137.7 with SMTP id v7ls3460798pfd.7.gmail; Sun, 19 Nov 2017 19:13:01 -0800 (PST) X-Received: by 10.159.204.147 with SMTP id t19mr4705617plo.47.1511147581566; Sun, 19 Nov 2017 19:13:01 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1511147581; cv=none; d=google.com; s=arc-20160816; b=mMpme8NHXYbkh8KgxUlTsqeQu0cDvBP3zVslBYgxjve/EJLiPT0QwPyrUcx9+6XZ8V zNnAVjqojXaUsz0pkUIz1hExIS2RWP8PyMBYy982YvEuZsvr3E/sL8bAvhNIrkuFiRsF mVhelYcPvHUIokerDDC8YjFc8ivXOWei/p44WTuFIjcJ8FRFykFMhF5tWgO2+j9zfwMi 0KL8S224es1N7PxmUmlWahFF99e0gT9ltNXvIiaDDMRaudZtOdO+VZI8uhF2cMznhtQv PEX6U3TMqhn9kji/f2fdbEnVWLBRBzVKKyOw6u+yFJ35cj+A+36Q4XcilRFFbm5kuFiA Ubrw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:cc:date:message-id:subject:mime-version :content-transfer-encoding:from:dkim-signature :arc-authentication-results; bh=R2yJwoTQ01dC+KUJUCEr7yCMOaYNYCN4xVUi3b3Llk4=; b=Numc3xHk2VqDzkctQKN/xO7S7UIGm5R5xM6RlRyqlWfOCoWiH4ATwOK/u0b59Z59IK FGb9Cgkh7jKQfpDP2WwPXjX94z5mJPPB0W57aHnGaFqOWrAkQqCcN6GRSxrgaEMqUoRU gs5+NU5TLgeyciOatD+HwRj4KbJSpp1aMQqaTnhgRMNR1MyvIWAOOFlh8+CEPZDOR4JQ esC4V0rPrb/LV4Yh7NaXv/EyhAL/yrJWb6wGfPbVA2s6bQxnSM5L5n4/4PEzD3jG7EGw TjhOQ/ChL5gaI7Jmmy4hjQvQtR9nxbLSBn58OYli3hIy7jkesKLiYQ4w4qhVEnp4fMfH ViJw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=OtFUWRNW; spf=neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-qt0-x236.google.com (mail-qt0-x236.google.com. [2607:f8b0:400d:c0d::236]) by gmr-mx.google.com with ESMTPS id a21si165800pgw.5.2017.11.19.19.13.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 19 Nov 2017 19:13:01 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) client-ip=2607:f8b0:400d:c0d::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=OtFUWRNW; spf=neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qt0-x236.google.com with SMTP id u42so13191501qte.7 for ; Sun, 19 Nov 2017 19:13:01 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=from:content-transfer-encoding:mime-version:subject:message-id:date :cc:to; bh=R2yJwoTQ01dC+KUJUCEr7yCMOaYNYCN4xVUi3b3Llk4=; b=OtFUWRNW+6wl3ufhmICHrM7GZHTNf56kFmC/j+yiQUhFBEvEsWpVsYL+P8sRhWEVyf UuK8M85ChAea1tOYVmoOPURHG2RABHsAblQKRqMDZRvwsnHKnobsLPXH3NLFNYO1QzEa SJnYRudKD8zRPDOR3rZ0cHG4s8Y9Bwmp0IcR0yQ4fMIyHgHxu5KXkCIqERjNGcaeyrCL Gu0S1aJ1I0VssF5Ki9KNyZk/qXUtKNY+jzwafWkDdzi4obKKDcfiFhw2hYI/SDf+0NH+ txYGO0D6jjaoBdg5dkkYIwvGla5aiMgO0yjNX53oAYxRqUHwP5gIM5Mubx2jrhp8KW9h +egQ== X-Gm-Message-State: AJaThX5779uTztiIVWmZHPACZ95gJdV2XlcpzoYiMPpASus3kckAHxFn 3QWWiOQZv2zmlk1s2SvkvKVrjvh9moE= X-Received: by 10.200.28.82 with SMTP id j18mr19890005qtk.133.1511147580652; Sun, 19 Nov 2017 19:13:00 -0800 (PST) Return-Path: Received: from steveawodeysair.home (pool-74-98-210-201.pitbpa.fios.verizon.net. [74.98.210.201]) by smtp.gmail.com with ESMTPSA id q26sm6438222qkl.77.2017.11.19.19.12.59 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 19 Nov 2017 19:12:59 -0800 (PST) From: Steve Awodey Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) Subject: PhD positions at CMU Message-Id: <45FCFEA8-B8BF-405B-A6A3-5387295BDE0E@cmu.edu> Date: Sun, 19 Nov 2017 22:12:59 -0500 Cc: Steve Awodey , Jeremy Avigad To: Homotopy Type Theory X-Mailer: Apple Mail (2.3273) The Homotopy Type Theory research group at CMU Philosophy has positions ope= n in the coming academic year 2018-19 for incoming PhD students interested = in doing research in type theory, homotopy theory, (higher) category theory= , and related areas. For more information about our very active research g= roup, see the info page here: https://cmuhott.wordpress.com/ The department also has a research group focused on interactive theorem pro= ving, formal verification, and formalization of mathematics, centered on th= e Lean Theorem Prover: https://leanprover.github.io/ For information about the Pure and Applied Logic PhD program at CMU, see th= e info page here: https://www.cmu.edu/dietrich/philosophy/graduate/phd/pure-and-applied-logic= /index.html Admitted students receive full tuition, a generous living stipend, health i= nsurance, and other benefits. Students are typically assigned limited teac= hing duties as graders or teaching assistants, or, when available, are supp= orted by a research grant. Upon completion of the program, students receive= the degree of PhD in Pure and Applied Logic. For further information, ple= ase contact Steve Awodey (awo...@cmu.edu) or Jeremy Avigad (avi...@cmu.edu)= . Deadline: January 2, 2018