Hi, I'm looking for a postdoc, and can currently offer a position until January 2021 (inclusive). You'll be joining me at the Laboratory for the Foundations of Computer Science (LCFS) at the School of Informatics in the University of Edinburgh. We'll be looking at the semantic foundations of computational effects and the foundations of statistical probabilistic programming. More details here, with a brief summary below: https://www.vacancies.ed.ac.uk/pls/corehrrecruit/erq_jobspec_version_4.jobsp... I'm at POPL this week --- in case you're here and want to chat. Otherwise, just email me. If you're not currently looking for a postdoc position, but know someone who is, please forward this information to them. Yours, Ohad. --------------------------------------------------------- Closing date: Friday 15th February 2019 at 5pm (GMT) Interviews (expected): 27 or 28 February 2019 Project Information Programs exhibit implicit behaviour, such as I/O and state interaction, probabilistic non-determinism, Bayesian conditioning, and gradient manipulation, under the umbrella term 'computational effects'. Computational effects pose challenges in modelling and reasoning about programs, as their interaction with other programming language theories, such as higher-order structure and polymorphism, is still poorly understood. Axiomatics is a highly successful technique in reasoning about computational effects. In this project, you will conduct basic research into the connections between axiomatics and denotational modelling of computational effects. You will also specialise this theory towards the foundations of probabilistic programming. Essential criteria * Completed, or near completion of, a PhD in computer science or mathematics, or equivalent experience. * Demonstrable experience in denotational modelling of programming languages. * Demonstrable working knowledge in category theory. * Demonstrable working knowledge in domain theory. * Ability to communicate clearly complex technical material orally and in writing. Desirable criteria * Experience with axiomatic verification of higher-order programs with effects. * Demonstrable working knowledge in refinement type systems and their mathematical models. * Demonstrable working knowledge in measure theory, probability, and statistics. * Demonstrable experience in programming with and/or modelling effect handlers. * Demonstrable experience in programming in and/or modelling statistical probabilistic programming languages * Experience in publication and presentation in international programming language venues. * Demonstrable knowledge in designing and solving recursive domain equations. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]