[TYPES/announce] Post doc at IT University of Copenhagen

[Rasmus Ejlers Møgelberg]

Dear all,

I have an available post doc position at the IT University of Copenhagen. My funding covers two years, but for administrative reasons the contract will be initially for one year with the possibility of extension for one more. Ideally, I would like the post doc to start in August, but I realize that this is a very short notice, so the starting date can be postponed until January 1st if needed.

The post doc will work on a project on guarded recursion, which is an approach to the problem of augmenting type theory with recursion without breaking consistency. Perhaps more accurately, it can be described as a synthetic approach to step-indexing with applications also to the problem om checking productivity of coinductive definitions. We are currently working on rewrite semantics and an implementation of an extension of cubical type theory with guarded recursion. I would prefer to hire someone who can work on these projects, but there is also work to be done on category theoretic models of guarded recursion, and so people with skills in the area of category theoretic models of type theory are also encouraged to apply. 

Those interested in the post doc should contact me via email as soon as possible.

Best wishes,
Rasmus Mogelberg