Ohad Kammar

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.

Current projects I currently hold a Royal Society University Research Fellowship on Foundations for type-driven data science. The current project member is Justus Matthiesen. I am a Creator on an ARIA Safeguarded AI grant Qbs4Safety: Core Representation Underlying Safeguarded AI. Other project members are Jesse Sigal and Justus Matthiesen. 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 involved with Ehud Lamm’s Conceptual Biology Lab. Past projects During 2019-2023 I undertook the first part of my Royal Society University Research Fellowship concerning effectful theories of programming languages: models, abstractions, validation, and axiomatics. The project members were Kasia Marek, Justus Matthiesen, James McKinna, Philip Saville, and Craig McLaughlin. During 2021-2022 I was 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. Project members were 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. During 2018-2019 I am worked 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. During 2017-2018, I held a Career Development Felowship in polymorphic effects at Balliol College Oxford. During 2016-2018 I worked with Sam Staton on his Royal Society-EPSRC funded project thanks to the Engineering and Physical Sciences Research Council and the Royal Society. During 2014-2016 I worked with Glynn Winskel on Events, Causality and Symmetry — the next generation semantics thanks to the European Research Council. During 2013-2014 I worked with Peter Sewell on Semantic Foundations for Real-World Systems, with close interaction with the participants of Rigorous Engineering for Mainstream Systems thanks to the Engineering and Physical Sciences Research Council. During 2012-2013 I worked with Sam Staton on algebraic theories, computational effects, and concurrency, thanks to the Isaac Newton Trust. During 2009-2013 I worked with Gordon D. Plotkin on my PhD thesis an algebraic theory of type and effect systems, thanks to the Scottish Informatics and Computer Science Alliance and the University of Edinburgh Informatics Graduate School.

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 Trace semantics Access control Staging and metaprogramming Partially-static data structures Reflection Conceptual biology Coevolution Drift The Baldwin effect

Publications and preprints (abstracts)

• Two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics, Preprint.
  Yotam Dvir, Ohad Kammar, Ori Lahav, and Gordon Plotkin. .

• A Denotational Approach to Release/Acquire Concurrency, Preprint.
  Yotam Dvir, Ohad Kammar, and Ori Lahav. .

• 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/978-3-031-57267-8_5, DOI: 10.1007/978-3-031-57267-8_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 Shared-State Concurrency, APLAS’22.

  Yotam Dvir, Ohad Kammar, and Ori Lahav. An Algebraic Theory for Shared-State 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/978-3-031-21037-2_1, DOI: 10.1007/978-3-031-21037-2_1.

• Frex: dependently-typed algebraic simplification, Preprint.
  Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop. , draft manuscript.

  Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop. 2022..

• Fully abstract models for effectful lambda-calculi via category-theoretic logical relations, POPL’22 (video, short video).

  Ohad Kammar, Shin-ya 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, NLP-CCS’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.nlpcss-1.14.

• On the expressive power of user-defined 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: Post-Proceedings 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. Partially-Static 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 type-and-effect 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 user-defined 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:1-13:29 (2017), arXiv:1610.09161, DOI: 10.1145/3110257.

• A convenient category for higher-order 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 omega-complete 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 978-3-95977-017-0, LIPICS Vol. 59.

• Semantics for probabilistic programming: higher-order 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 525-534, arXiv:1601.04943, DOI: 10.1145/2933575.2935313.

• An absolute characterisation of locally determined omega-colimits, Preprint.
  Ohad Kammar. , Proposal accepted to Domains XI.

  Ohad Kammar. 2014. Domains XI 2014 Workshop, arXiv:1508.05072.

• Inferring Co-Evolution, Philosophy of Science.

  Ehud Lamm and Ohad Kammar. 2014. Philosophy of Science Vol. 81, No. 4 (October), pp. 592-611. Published by: The University of Chicago Press on behalf of the Philosophy of Science Association, DOI: 10.1086/678045.

• An algebraic theory of type-and-effect systems, Ph.D. thesis.

  Ohad Kammar. 2014. Ph.D. thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, UK.

• Handlers in Action, ICFP’13.

  Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Proceedings of the 18th ACM SIGPLAN international conference on Functional programming Pages 145-158, ISBN 978-1-4503-2326-0, DOI: 10.1145/2544174.2500590.

• Algebraic Foundations for Effect-Dependent Optimisations, POPL’12.

  Ohad Kammar and Gordon D. Plotkin. 2012. Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages Pages 349-360, ISBN: 978-1-4503-1083-3, 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/978-3-642-22944-2_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 self-proposed project involving some of my research interests.

See my teaching page for more information about:

• Undergraduate-level course type-driven probabilistic modelling (under development);
• MSc projects;
• undergraduate (UG4/MInf) projects; and
• Other past teaching activities.

Talks (abstracts)

• A Type-Driven Overview of Probabilistic Programming, University of Tartu Programming Languages Research Seminar, 28 October, 2024.

• Semantic foundations for type-driven probabilistic modelling, 40th International Conference on Mathematical Foundations of Programming Semantics (MFPS’24), 21 June, 2024.

• Semantic foundations of potential-synthesis for expected amortised-cost analysis, 11th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE’23), 04 September, 2023.

• Frex: staged-optimisation and equational-proof-synthesis using universal algebra, 21st meeting of IFIP Working Group 2.11: Program Generation, 16 August, 2022.

• An introduction to statistical modelling semantics with higher-order measure theory, Logic of Probabilistic Programming, see course webpage for latest recordings and exercise sheets, 03 February, 2022.

• Frex: dependently-typed 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.

• Higher-order building blocks for statistical modelling, PPS-PIHOC-DIAPASoN Workshop, 17 February, 2021.

• An introduction to ProbProg, Huawei Tech-Talk, Huawei Edinburgh Research Centre, 14 January, 2021.

• Frex: indexing-modulo-equations 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: indexing-modulo-equations 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’Hearn-Reicke model, Syntax and Semantics of Low-Level Languages (LOLA’19), 23 June, 2019.

• Where do ideas come from?, 4th Logic Mentoring Workshop, affiliated with LICS’19, 11 April, 2019.

• Eff-Bayes: modular implementations of approximate Bayesian inference with effect handlers, School of Computing, KAIST, 11 April, 2019.

• A tutorial on quasi-Borel spaces, Department of Computer Science, the University of British Columbia, 22 March, 2019.

• A tutorial on quasi-Borel spaces, Workshop on Higher-order probabilistic computation, Bellairs Research Institute, 17 March, 2019.

• Eff-Bayes: modular implementations of approximate Bayesian inference with effect handlers, Scottish Programming Language Seminar, University of St. Andrews School of Computer Science](https://www.cs.st-andrews.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 Higher-Order Computation (PIHOC), 07 February, 2019.

• A domain theory for statistical probabilistic programming, LSV Seminar, Laboratoire Spécification et Vérification, École normale supérieure Paris-Saclay, Paris, 29 January, 2019.

• A domain theory for statistical probabilistic programming, 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, 23 September, 2018.

• A domain theory for quasi-Borel 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, Friedrich-Alexander-Universität Erlangen-Nürnberg, 25 June, 2018.

• A domain theory for quasi-Borel 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.

• Quasi-Borel spaces and the validation of Bayesian inference algorithms, Workshop on Probabilistic Interactive and Higher-Order Computation (PIHOC), 22 February, 2018.

• On the expressive power of user-defined 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 higher-order probability theory, 32st Annual ACM/IEEE Symposium on Logic in Computer Science, 20 June, 2017.

• Quasi Borel-spaces, 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 user-defined effects: effect handlers, monadic reflection, delimited control without answer-type-modification, LSD Seminar, Programming, Logic, and Semantics Group, University of Cambridge Computer Laboratory, 17 February, 2017.

• On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control without answer-type-modification, 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 (S-REPLS4), 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 Low-Level 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 Hindley-Milner Polymorphism, 4th ACM SIGPLAN Workshop on Higher-Order 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 omega-colimits, Domains XI Workshop, 09 September, 2014.

• Graphical algebraic foundations for monad stacks, 3rd ACM SIGPLAN Workshop on Higher-Order 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 type-and-effect 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 Higher-Order Programming with Effects (HOPE’12), 09 September, 2012.

• Handlers in Action, Scottish Programming Lanugage Seminar (SPLS), 15 March, 2012.

• Algebraic Foundations for Effect-Dependent Optimisations, Principles of Programing Seminar (POP), 30 January, 2012.

• Algebraic Foundations for Effect-Dependent Optimisations, 39th Symposium on Principles of Programming Languages (POPL’12), 26 January, 2012.

• Algebraic Foundations for Effect-Dependent 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 Cartwright-Felleisen-Wadler conjecture, talk proposal accepted to, and delivered by Dylan McDermott the Workshop on Higher-Order 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, Thirty-Ninth 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 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

• Co-organise 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 Co-chair, Languages for Inference (LAFI, né PPS), with Jeffery Siskind. Submit a talk proposal!

• Committee member, Royal Society International Exchanges Committee, 2019-2021.

2018

• PC member, 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS) 2018. Submit a paper!

• PC Co-chair, Workshop on Syntax and Semantics of Low-Level 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 Low-Level Languages (LOLA’17).

• Co-organise the fifth South-Regional English Programming Language Seminar (S-REPLS) with Prof Jeremy Gibbons and Dr. Sam Staton.

2016

• Co-organised the International Summer School on Metaprogramming with Dr. Jeremy Yallop and Ms. Gemma Gordon.

2015 - 2018

• Co-founder and steering committee member of the South-Regional English Programming Language Seminar (S-REPLS) with Dr. Dominic Mulligan and Dr. Jeremy Yallop.

2014

• PC member, 3rd ACM SIGPLAN Workshop on Higher-Order 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.

• Co-organised the Haskell Symposium’s ``Future of effects in Haskell’’ panel with Sam Lindley.

• Co-organised 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 2-upped 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.