Dear all, I have recently received a grant from the Danish Council for Independent Research to hire a post doc to work on guarded recursive types in type theory. Ideally, I would like to find someone who has both knowledge of categorical models of type theory and practical experience with proof assistants. The job is initially for one year, but with the possibility of extension for another two. Those interested should contact me. More details can be found here: https://delta.hr-manager.net/ApplicationInit.aspx?cid=119&departmentId=3439&ProjectId=180662&MediaId=5 Rasmus Mogelberg [For admin and other information see: http://www.mta.ca/~cat-dist/ ]