[TYPES/announce] Research associate in computational effects modelling and axiomatics

[KAMMAR Ohad]

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.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20190117/585cd86b/attachment.html>