[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
