ContactOffice 3.11 To schedule an appointment, consult my calendar. 

Current projectsI 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 Kasia Marek, Justus Matthiesen, James McKinna, Philip Saville, and Craig McLaughlin. I am a coinvestigator 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 coordinated with Erik Meijer, Satish Chandra at Facebook. I am also involved with Ehud Lamm’s Conceptual Biology Lab. Past projects

Research interests

Publications and preprints (abstracts)
A Denotational Approach to Release/Acquire Concurrency, Preprint.
A Denotational Approach to Release/Acquire Concurrency, ESOP’24.
Yotam Dvir, Ohad Kammar, and Ori Lahav. A Denotational Approach to Release/Acquire Concurrency. In: Weirich, S. (eds) Programming Languages and Systems. ESOP 2024. Lecture Notes in Computer Science, vol 14577. Springer, Cham. https://doi.org/10.1007/9783031572678_5, DOI: 10.1007/9783031572678_5.
Shoggoth: A Formal Foundation for Strategic Rewriting, POPL’24 (video).
Xueying Qin, Liam O’Connor, Rob van Glabbeek, Peter Hoefner, Ohad Kammar, and Michel Steuwer. Proc. ACM Program. Lang. 8, POPL, Article 3 (January 2024), 28 pages. DOI:https://doi.org/10.1145/3633211, DOI: 10.1145/3633211.
An Algebraic Theory for SharedState Concurrency, APLAS’22.
Yotam Dvir, Ohad Kammar, and Ori Lahav. An Algebraic Theory for SharedState Concurrency. In: Sergey, I. (eds) Programming Languages and Systems. APLAS 2022. Lecture Notes in Computer Science, vol 13658. Springer, Cham. https://doi.org/10.1007/9783031210372_1, DOI: 10.1007/9783031210372_1.
Frex: dependentlytyped algebraic simplification, Preprint, draft manuscript.
Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop. 2022..
Fully abstract models for effectful lambdacalculi via categorytheoretic logical relations, POPL’22 (video, short video).
Ohad Kammar, Shinya Katsumata, and Philip Saville. Proc. ACM Program. Lang. 6, POPL, Article 44 (January 2022), 28 pages. DOI:https://doi.org/10.1145/3498705, DOI: 10.1145/3498705.
Recalibrating classifiers for interpretable abusive content detection, NLPCCS’20.
Bertie Vidgen, Sam Staton, Scott A. Hale, Ohad Kammar, Helen Margetts, Tom Melham, Marcin Szymczak. 2020. In Proceedings of the Fourth Workshop on Natural Language Processing and Computational Social Science, pages 132–138, Online. Association for Computational Linguistics., DOI: 10.18653/v1/2020.nlpcss1.14.
On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control (updated version), JFP (video).
Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. 2019. Journal of Functional Programming Special Issue: PostProceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming, to appear, arXiv:1610.09161, DOI: 10.1145/3110257.
A Domain Theory for Statistical Probabilistic Programming, winner of the POPL’19 Distinguished Paper Award (video).
Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A Domain Theory for Statistical Probabilistic Programming. Proc. ACM Program. Lang. 3, POPL, Article 36 (January 2019), 35 pages., DOI: 10.1145/3290349.
Partially static data as free extension of algebras, ICFP’18.
Jeremy Yallop, Tamara von Glehn, Ohad Kammar. 2018. PartiallyStatic Data as Free Extension of Algebras. Proc. ACM Program. Lang. 2, ICFP, Article 100 (September 2018), 30 pages., DOI: 10.1145/3236795.
Functional programming for modular Bayesian inference, ICFP’18.
Adam Ścibior Ohad Kammar, and Zoubin Ghahramani. 2018. Adam Ścibior, Ohad Kammar, and Zoubin Ghahramani. 2018. Functional Programming for Modular Bayesian Inference. Proc. ACM Program. Lang. 2, ICFP, Article 83 (September 2018), 29 pages., DOI: 10.1145/3236778.
Factorisation systems for logical relations and monadic lifting in typeandeffect system semantics, MFPS’18.
Ohad Kammar and Dylan McDermott. 2018. 34th Conference on the Mathematical Foundations of Programming Semantics, accepted for publication, arXiv:1804.03460, DOI: 10.1016/j.entcs.2018.11.012.
Denotational validation of Bayesian inference, POPL’18 (video).
Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani. 2018. Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, PACMPL 2(POPL), Article 60, arXiv:1711.03219, DOI: 10.1145/3158148.
On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control, ICFP’17 (video).
Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. 2017. Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming, PACMPL 1(ICFP): 13:113:29 (2017), arXiv:1610.09161, DOI: 10.1145/3110257.
A convenient category for higherorder probability theory, LICS’17.
Chris Heunen, Ohad Kammar, Sam Staton, Hongseok Yang. 2017. Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, arXiv:1701.02547, DOI: 10.1109/LICS.2017.8005137.
A monad for full ground reference cells, LICS’17.
Ohad Kammar, Paul Blain Levy, Sean Keith Moss, Sam Staton. 2017. Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, arXiv:1702.04908, DOI: 10.1109/LICS.2017.8005109.
No value restriction is needed for algebraic effects and handlers, JFP, based on this Twelf formalisation.
Ohad Kammar and Matija Pretnar. 2017. Journal of Functional Programming Volume 27. Cambridge University Press, DOI: 10.1017/S0956796816000320.
Bayesian inversion by omegacomplete cone duality, CONCUR’16, invited paper.
Fredrik Dahlqvist, Vincent Danos, Ilias Garnier, and Ohad Kammar. 2016. 27th International Conference on Concurrency Theory, Josée Desharnais and Radha Jagadeesan (Eds.), ISBN 9783959770170, LIPICS Vol. 59.
Semantics for probabilistic programming: higherorder functions, continuous distributions, and soft constraints, LICS’16.
Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, and Frank Wood. 2016. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science Pages 525534, arXiv:1601.04943, DOI: 10.1145/2933575.2935313.
An absolute characterisation of locally determined omegacolimits, Preprint, Proposal accepted to Domains XI.
Ohad Kammar. 2014. Domains XI 2014 Workshop, arXiv:1508.05072.
Inferring CoEvolution, Philosophy of Science.
Ehud Lamm and Ohad Kammar. 2014. Philosophy of Science Vol. 81, No. 4 (October), pp. 592611. Published by: The University of Chicago Press on behalf of the Philosophy of Science Association, DOI: 10.1086/678045.
An algebraic theory of typeandeffect systems, Ph.D. thesis.
Ohad Kammar. 2014. Ph.D. thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, UK.

Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Proceedings of the 18th ACM SIGPLAN international conference on Functional programming Pages 145158, ISBN 9781450323260, DOI: 10.1145/2544174.2500590.
Algebraic Foundations for EffectDependent Optimisations, POPL’12.
Ohad Kammar and Gordon D. Plotkin. 2012. Proceedings of the 39th annual ACM SIGPLANSIGACT symposium on Principles of programming languages Pages 349360, ISBN: 9781450310833, DOI: 10.1145/2103656.2103698.
On the statistical thermodynamics of reversible communicating processes, CALCO’11, invited paper.
Giorgio Bacci, Vincent Danos and Ohad Kammar. 2011. Algebra and Coalgebra in Computer Science. Corradini A., Klin B., Cîrstea C. (Eds.). Lecture Notes in Computer Science, vol 6859. Springer, Berlin, Heidelberg, DOI: 10.1007/9783642229442_1.
Teaching
I supervise UG4/MInf and MSc projects in the School of Informatics. Please get in touch if you’d like to explore a selfproposed project involving some of my research interests.
See my teaching page for more information about:
 Undergraduatelevel course typedriven probabilistic modelling (under development);
 MSc projects;
 undergraduate (UG4/MInf) projects; and
 Other past teaching activities.
Talks (abstracts)
Semantic foundations for typedriven probabilistic modelling, 40th International Conference on Mathematical Foundations of Programming Semantics (MFPS’24), 21 June, 2024.
Semantic foundations of potentialsynthesis for expected amortisedcost analysis, 11th ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE’23), 04 September, 2023.
Frex: stagedoptimisation and equationalproofsynthesis using universal algebra, 21st meeting of IFIP Working Group 2.11: Program Generation, 16 August, 2022.
An introduction to statistical modelling semantics with higherorder measure theory, Logic of Probabilistic Programming, see course webpage for latest recordings and exercise sheets, 03 February, 2022.
Frex: dependentlytyped algebraic simplification, Scottish Programming Languages Seminar, 20 October, 2021.
Where do ideas come from?, Mental Strength for Science Unworkshop, 17 August, 2021.
Tutorial: equational reasoning and rewriting, Idris Developers Meeting 2021, 28 February, 2021.
Higherorder building blocks for statistical modelling, PPSPIHOCDIAPASoN Workshop, 17 February, 2021.
An introduction to ProbProg, Huawei TechTalk, Huawei Edinburgh Research Centre, 14 January, 2021.
Frex: indexingmoduloequations with free extensions (video), Seminar on the Foundations of Mathematics and Theoretical Computing, Faculty of Mathematics and Physics, University of Ljubljana, 15 October, 2020.
Frex: indexingmoduloequations with free extensions, Programming Languages at University of Glasgow (PLUG) Seminar, School of Computing Science, University of Glasgow, 13 October, 2020.
A ProbProg Language Taxonomy, 36th International Conference on Mathematical Foundations of Programming Semantics (MFPS’20) Special Session on Probabilistic Programming, 05 June, 2020.
A modern perspective on the O’HearnReicke model, Syntax and Semantics of LowLevel Languages (LOLA’19), 23 June, 2019.
Where do ideas come from?, 4th Logic Mentoring Workshop, affiliated with LICS’19, 11 April, 2019.
EffBayes: modular implementations of approximate Bayesian inference with effect handlers, School of Computing, KAIST, 11 April, 2019.
A tutorial on quasiBorel spaces, Department of Computer Science, the University of British Columbia, 22 March, 2019.
A tutorial on quasiBorel spaces, Workshop on Higherorder probabilistic computation, Bellairs Research Institute, 17 March, 2019.
EffBayes: modular implementations of approximate Bayesian inference with effect handlers, Scottish Programming Language Seminar, University of St. Andrews School of Computer Science](https://www.cs.standrews.ac.uk/), 13 March, 2019.
A domain theory for statistical probabilistic programming, Logic and Semantics Seminar, Programming, Logic, and Semantics Group, University of Cambridge Computer Laboratory, 22 February, 2019.
A domain theory for statistical probabilistic programming, Seminar za temelje matematike in teoretično računalništvo, Faculty of Mathematics and Physics, University of Ljubljana, 14 February, 2019.
A domain theory for statistical probabilistic programming, Second Workshop on Probabilistic Interactive and HigherOrder Computation (PIHOC), 07 February, 2019.
A domain theory for statistical probabilistic programming, LSV Seminar, Laboratoire Spécification et Vérification, École normale supérieure ParisSaclay, Paris, 29 January, 2019.
A domain theory for statistical probabilistic programming, 7th ACM SIGPLAN Workshop on HigherOrder Programming with Effects, 23 September, 2018.
A domain theory for quasiBorel spaces and statistical probabilistic programming, invited talk, International Workshop on Domain Theorey and its Applications, 08 July, 2018.
A monad for full ground reference cells, Theoretische Informatik Seminar, Department of Computer Science, Faculty of Engineering, FriedrichAlexanderUniversität ErlangenNürnberg, 25 June, 2018.
A domain theory for quasiBorel spaces, Oxford Quantum Day 2018, 19 June, 2018.
Modular Bayesian inference, Dagstuhl seminar 18172: algebraic effects go mainstream, 24 April, 2018.
Denotational validation of Bayesian inference, Mobility Reading Group Seminar, Department of Computing, Imperial College London, 11 April, 2018.
QuasiBorel spaces and the validation of Bayesian inference algorithms, Workshop on Probabilistic Interactive and HigherOrder Computation (PIHOC), 22 February, 2018.
On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control (video), 22nd ACM SIGPLAN International Conference on Functional Programming, 04 September, 2017.
Denotational validation of Bayesian inference, Séminaire PLUME École normale supérieure de Lyon, 12 July, 2017.
A monad for full ground reference cells, 32st Annual ACM/IEEE Symposium on Logic in Computer Science, 23 June, 2017.
A convenient category for higherorder probability theory, 32st Annual ACM/IEEE Symposium on Logic in Computer Science, 20 June, 2017.
Quasi Borelspaces, University of Oxford Department of Computer Science Quantum Group Workshop, 13 May, 2017.
A monad for full ground reference cells, Oxford Advanced Seminar on Informatic Structures (OASIS), Foundations Logic and Structures theme, University of Oxford Department of Computer Science, 10 March, 2017.
A monad for full ground reference cells, Logic and Semantics Seminar, Programming, Logic, and Semantics Group, University of Cambridge Computer Laboratory, 17 February, 2017.
On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control without answertypemodification, LSD Seminar, Programming, Logic, and Semantics Group, University of Cambridge Computer Laboratory, 17 February, 2017.
On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control without answertypemodification, Mathematically Structured Programming Group, University of Strathclyde Computer and Information Sciences Department, 06 February, 2017.
A monad for full ground reference cells, LFCS Seminar, Laboratory for Foundations of Computer Science, University of Edinburgh School of Informatics, 31 January, 2017.
On the Expressive Power of Algebraic Effects and Handlers, 4th South of England Regional Programming Language Seminar (SREPLS4), Imperial College London, 27 September, 2016.
Functional models of full ground, and general, reference cells (video), HOPE’16 Workshop, 18 September, 2016.
No value restriction is needed for algebraic effects and handlers, Syntax and Semantics of LowLevel Languages (LOLA’16), 10 July, 2016.
No value restriction is needed for algebraic effects and handlers, Seminaire Gallium, INRIA Paris Rocquencourt, France., 17 June, 2016.
No value restriction is needed for algebraic effects and handlers, ANTIQUE seminar, École normale supérieure, Paris, France., 16 June, 2016.
No value restriction is needed for algebraic effects and handlers, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), 26 May, 2016.
No value restriction is needed for algebraic effects and handlers, Logic and Semantics group seminar, Department of Computer Science, University of Aarhus, Denmark., 21 March, 2016.
No value restriction is needed for algebraic effects and handlers, Schloss Dagstuhl Seminar ‘From theory to practice of algebraic effects and handlers’, 18 March, 2016.
A denotational semantics for HindleyMilner Polymorphism, 4th ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE’15), 30 August, 2015.
A syllabus for algebraic effects (invited tutorial), Mathematical Foundations of Programming Semantics XXXI (MFPS’15), 25 June, 2015.
A universal characterisation of locally determined omegacolimits, Domains XI Workshop, 09 September, 2014.
Graphical algebraic foundations for monad stacks, 3rd ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE’14), 31 August, 2014.
Graphical algebraic foundations for monad stacks, Electronic and Software Systems seminar, University of Southhampton, 30 July, 2014.
Graphical algebraic foundations for monad stacks, University of Edinburgh LFCS PLInG, 02 June, 2014.
Graphical algebraic foundations for monad stacks, University of Strathclyde MSP 101 seminar series, 28 May, 2014.
An algebraic theory of type and effect systems, University of Cambridge Computer Laboratory Logic and Semantics Seminar, 13 December, 2013.
An algebraic theory of type and effect systems, MIT Programming Languages Seminar, 30 September, 2013.
A general theory of typeandeffect systems via universal algebra, Journées d’Informatique Fondamentale de Paris Diderot, 25 April, 2013.
An introduction to Programming Language Semantics, 1st join category theory and computer science seminar, University of Cambridge, 18 November, 2012.
Handlers in Action, 1st ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE’12), 09 September, 2012.
Handlers in Action, Scottish Programming Lanugage Seminar (SPLS), 15 March, 2012.
Algebraic Foundations for EffectDependent Optimisations, Principles of Programing Seminar (POP), 30 January, 2012.
Algebraic Foundations for EffectDependent Optimisations, 39th Symposium on Principles of Programming Languages (POPL’12), 26 January, 2012.
Algebraic Foundations for EffectDependent Optimisations, Functional Programming Lab Seminar, 11 January, 2012.
Programming Language Semantics: {Ret  Int  P}rospective Discussion, LFCS Lab Lunch, 20 September, 2011.
Algebraic Foundations for Type and Effect Analysis, European Workshop on Computational Effects, 18 March, 2011.
Take Action for Your State!, joint Scottish Programming Lanugage Seminar (SPLS) and Fun in the Afternoon, 24 November, 2010.
A well kept secret…, LFCS Lab Lunch, 19 January, 2010.
Reports (abstracts)
Foundations for Probabilistic Programming, Poster presented at the 1st Probabilistic Programming Conference, 19 June, 2018.
A monadic solution to the CartwrightFelleisenWadler conjecture, talk proposal accepted to, and delivered by Dylan McDermott the Workshop on HigherOrder Programming with Effects (HOPE’17), 03 September, 2017.
Algebraic Approaches to Semantics, Research Proposal, 24 February, 2010.
Upcoming gigs
Attending Scottish Programming Languages and Verification Summer School 2019 in Mathematically Structured Programming Group, University of Strathclyde, Glasgow, Scotland , 05 August, 2019 to 09 August, 2019.
Attending 2nd International Summer School on Metaprogramming in Schloss Dagstuhl, Germany , 11 August, 2019 to 16 August, 2019.
Attending International Conference on Functional Programming and affiliated events in Berlin, Germany , 18 August, 2019 to 23 August, 2019.
Attending Languages for Inference (LAFI 2019) in New Orleans, Oregon , 21 January, 2020.
Community service
2024
PC member, ThirtyNinth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), which will take place in Tallinn (Estonia), July, 2024. Submit a paper!.
PC member, POPL Student Research Competition, which will take place in London (England), January, 2024. Submit an entry!
2023
Liberated Robin Grayson’s Intuitionistic set theory from the trees, with the help of Martín Escardó, Paul Levy and Paul Taylor, with the kind permission of Robin Grayson himself, the financial support of the Royal Society, and the legwork of the Bodleian staff.
PC member, 21st Asian Symposium on Programming Languages and Systems, which will take place in Taipei (Taiwan), Nov, 2023. Submit a paper!
2022
 Thanks to Christine Tasson’s valiant efforts, we now have a digital copy of Yves Lafont’s thesis. This liberation mission was initiated by Philip Saville with the moral support of James McKinna.
2020
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 Cochair, 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
Coorganise the International Summer School on Metaprogramming at Schloss Dagstuhl with Dr. Jeremy Yallop and Prof. Yukiyoshi Kameyama. Registration is now open!
External reviewing committee, 24th ACM SIGPLAN International Conference on Functional Programming. Submit a paper!
PC member, Asian Symposium on Programming Languages and Systems (APLAS 2019). Submit a paper!
PC Cochair, Languages for Inference (LAFI, né PPS), with Jeffery Siskind. Submit a talk proposal!
Committee member, Royal Society International Exchanges Committee, 20192021.
2018
PC member, 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS) 2018. Submit a paper!
PC Cochair, Workshop on Syntax and Semantics of LowLevel Languages (LOLA’18), with Prof. Patricia Johann. Submit an abstract! :)
PC member, Workshop on Probabilistic Programming Languages, Semantics, and Systems.
2017
Student Bursary Chair, Second International Conference on Formal Structures for Computation and Deduction (FSCD’17).
PC member, Workshop on Syntax and Semantics of LowLevel Languages (LOLA’17).
Coorganise the fifth SouthRegional English Programming Language Seminar (SREPLS) with Prof Jeremy Gibbons and Dr. Sam Staton.
2016
 Coorganised the International Summer School on Metaprogramming with Dr. Jeremy Yallop and Ms. Gemma Gordon.
2015  2018
 Cofounder and steering committee member of the SouthRegional English Programming Language Seminar (SREPLS) with Dr. Dominic Mulligan and Dr. Jeremy Yallop.
2014
 PC member, 3rd ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE’14).
2013
Liberated Robin Gandy’s thesis On Axiomatic Systems in Mathematics and Theories in Physics (OCR) from the trees. This deed was made possible with the kind help of Martin Hyland, the eager consent of the copyright holder, the literary executor Mike Yates, and the generous financial support of Barry Cooper.
Nachum Dershowitz supplied the OCR version.Coorganised the Haskell Symposium’s ``Future of effects in Haskell’’ panel with Sam Lindley.
Coorganised the Agda Course in Cambridge with Dr. Dominic Orchard.
Liberated algebra valued functors in general and tensor products in particular by Prof. Peter Freyd from the trees. I was unable to obtain Prof. Freyd’s permission to put this scan up, but the book that included it did not contain any copyright notice. If you know I am infringing on his copyright, please let me know.
2011
 Liberated Algebraic Theories (1969) by Prof. Gavin Wraith from the trees. With the kind permission of Prof. Wraith, this scan of his Aarhus University Lecture Notes can be freely circulated. A 2upped version.
 Organised the SICSA Agda Course by Conor McBride.
Media presence
 Interviewed for the Edinbugh University Informatics School CompuCast PodCast “Semantics, Semantics, Semantics”, November 2012.
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.