I now have available a 9-month post-doctoral research fellow position for research on the computational interpretation of homotopy type theory. I am looking for someone with a strong background in intuitionistic type theory and mechanized reasoning, and will prefer candidates with computer science credentials over those without. The foundation of the project is described at http://www.homotopytypetheory.org, and in particular the monograph mentioned therein. The official job posting is attached for your reference. It is intended that the successful candidate would begin work at the start of the fall semester at Carnegie Mellon, and continue for the academic year, but some small flexibility may be possible, with the permission of the funding agency. This project is funded by the National Science Foundation under grant number CCF-1116703. Robert Harper Professor, Computer Science [For admin and other information see: http://www.mta.ca/~cat-dist/ ]