Post-Doctoral Fellowship at CMU on Homotopy Type Theory

Post-Doctoral Fellowship at CMU on Homotopy Type Theory

[Robert Harper]

[-- Attachment #1: Type: text/plain, Size: 108 bytes --]

[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


[-- Attachment #2: Type: text/plain, Size: 911 bytes --]

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




[-- Attachment #3: PostDoc.txt --]
[-- Type: text/plain, Size: 2381 bytes --]

Job Description
 
Post Doctoral Fellow-100196

Description:
 
Carnegie Mellon University seeks applicants to fill the position of Post Doctoral Fellow in the Computer Science Department. Under the direction of the principal investigator, the incumbent will conduct and lead research in the field of theory of computation, particularly intuitionistic type theory and its application to homotopy theory. Specific duties will include conduct of fundamental research into the computational semantics of homotopy type theory with applications to programming languages and automated reasoning.  In addition, the successful candidate is expected to coordinate research with other members of the CMU community, as well as minimally supervise junior members of the group. The appointment is for one year with the possibility of renewal, pending available funding and satisfactory performance. 
 
Qualifications:
 
Minimum: \
•Education: Ph.D. in theoretical computer science or mathematics
 
•Experience: Strong background in: proof theory, category theory, categorial logic, type theory or related areas. Exeprience in: functional programming, semantics of programming languages, mechanized reasoning. 

•Skills: The successful candidate must have proven supervisory and leadership skills, and the ability to coordinate report findings and take lead in composing research proposals, specifically in response to broad agency announcements. Demonstrated ability to manage multiple priorities; and communicate effectively in an interdisciplinary environment. 

•Physical Mobility: Ability to travel to various campus locations as needed. Able to lift and bend and move equipment. May be required to work at computer for extended periods of time. 

•Mental: Must be able to communicate effectively in verbal, written and presentation forms. Ability to work under pressure, pay attention to detail, meet inflexible deadlines, and deal with difficult people while maintaining composure 

•Other: Normal office or laboratory environment
 
Department URL: http://www.cs.cmu.edu
 
To apply, use job number 100196:  http://www.cmu.edu/jobs/index.html
 
Primary Location: United States-Pennsylvania-Pittsburgh
 
FT/PT Status: Regular Full Time
 
Organization: COMPUTER SCIENCE DEPARTMENT
 
Minimum Education Level: Doctorate or equivalent
 
Salary: Negotiable