Ohad's Research - Home


Office 3.11
Bayes Centre
School of Informatics
University of Edinburgh
47 Potterrow
Edinburgh EH8 9BT
Tel: +44 (0)131 (6) 50 2960
Post: ohad.kammar@ed.ac.uk

To schedule an appointment, consult my calendar.

Current projects

I currently hold a Royal Society University Research Fellowship on effectful theories of programming languages: models, abstractions, validation, and axiomatics. Current and former project members are Justus Matthiesen, James McKinna, Philip Saville, and Craig McLaughlin.

I am a principal investigator on type-driven data-science infrastructure for Idris2, supported by the National Cyber Security Centre (NCSC) as part of the UK Research Institute in Verified Trustworhy Software Systems. Current project members are Robert Wright at the University of Edinburgh, Edwin Brady and Guillaume Allais at the University of St Andrews, and Jeremy Yallop at the University of Cambridge.

I am a co-investigator on differentiable probabilistic programming semantics, other project members are Luke Ong, Sam Staton, Matthijs Vákár, Maria I. Gorinova, and Jesse Sigal, thanks to Facebook Research. The project is co-ordinated with Erik Meijer, Satish Chandra at Facebook.

I am also currently working with Tom Melham, Sam Staton, Marcin Szymczak, Helen Margetts, and Scott Hale on probabilistic programming in the social sciences thanks to the Alan Turing Institute.

I am also involved with Ehud Lamm’s Conceptual Biology Lab.

Past projects

Research interests

  • Applied mathematics
    • Category theory
    • Logic
      • Ordinal notation systems
    • Universal algebra
  • Programming language theory
    • Semantics, in particular denotational semantics
    • Expressivity
    • Polymorphism
      • Value restriction
    • Computational effects
      • Effect type systems
      • Effect handlers
      • Delimited control
      • Monadic reflection
    • Domain theory
      • Axiomatisation
      • Probabilistic powerdomains
      • Jung-Tix problem
    • Probabilistic programming
      • Semantics
      • Structuring generative models
      • Variational inference and kernel methods
    • Concurrency
      • Event structures
      • Relaxed behaviour
    • Access control
    • Staging and metaprogramming
      • Partially-static data structures
  • Conceptual biology
    • Coevolution
    • Drift
    • The Baldwin effect

Publications and preprints (abstracts)

Teaching (Part III/Mphil projects, Part II projects, Courses)

Talks (abstracts)

Reports (abstracts)

Upcoming gigs

Community service



  • Sam Staton succeeded, where I failed, to liberated Johan Joss’s PhD thesis Algorithmisches Differenzierens from the trees. This effort was inspired by a talk given by Michele Pagani.

  • Liberated Rod Burstall’s Writing search algorithms in functional form from the trees.
    This deed was made possible with the kind help of Daniel Hillerström.
    Full citation:
    Burstall, R.M.: Writing search algorithms in functional form. In: Michie, D. (ed.) Machine Intelligence, vol. 3, pp. 373–385. Edinburgh University Press (1968).
    The original copy did not have a copyright notice. If you are aware of this copy infringing on a copyright, please get in touch.

  • PC member, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), which will take place in Paris (France), June/July, 2020. Submit a paper!

  • PC Co-chair, Languages for Inference (LAFI, né PPS), with Dougal Maclaurin. Submit a talk proposal!

  • PC member, ACM SIGPLAN Symposium on Principles of Programming Langages (POPL 2020). Submit a paper!





2015 - 2018




Media presence

Consultancy services

I provide private consultancy services at a limited capacity, separate from my role at the University. I am also able to offer more extensive consultancy services through the University.