Ohad's Research - Home

Contact

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.
profile

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 James McKinna, Philip Saville, and Craig McLaughlin.

I am a principle 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

2020

  • 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!

2019

2018

2017

2016

2015 - 2018

2014

2013

2011

Media presence

Consultancy

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 servirces through the University.