Research associate in computational effects modelling and axiomatics

Research associate in computational effects modelling and axiomatics

[Ohad Kammar]

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.jobspec?p_id=046553

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/ ]