The Homotopy Type Theory research group at CMU Philosophy has positions open 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 group, see the info page here: https://cmuhott.wordpress.com/ The department also has a research group focused on interactive theorem proving, formal verification, and formalization of mathematics, centered on the Lean Theorem Prover: https://leanprover.github.io/ For information about the Pure and Applied Logic PhD program at CMU, see the info page here: https://www.cmu.edu/dietrich/philosophy/graduate/phd/pure-and-applied-logic/... Admitted students receive full tuition, a generous living stipend, health insurance, and other benefits. Students are typically assigned limited teaching duties as graders or teaching assistants, or, when available, are supported by a research grant. Upon completion of the program, students receive the degree of PhD in Pure and Applied Logic. For further information, please contact Steve Awodey (awodey@cmu.edu) or Jeremy Avigad (avigad@cmu.edu). Deadline: January 2, 2018 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]