113 citations · 319 across the 18 of their papers we have counts for
20 papers
Finitary Semantics for Full Ground Local State
Orpheas van Rooij, Ohad Kammar, Sam Lindley +1
Full ground local state (FGLS) refers to dynamically allocated mutable state that allows storing ground values and references. It is a key ingredient in many imperative algorithms…
NSynC: Normalised Synthesis of Computation
Zoey Shepherd, Ohad Kammar, Elizabeth Polgreen
Inductive program synthesis algorithms search a space of programs to find one that meets some specification. Enumerating according to the syntax of a programming language leads to…
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
Ohad Kammar, Jack Liell-Cock, Sam Lindley +2
We use the theory of algebraic effects to give a complete equational axiomatization for dynamic threads. Our method is based on parameterized algebraic theories, which give a concr…
Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
Marcelo P. Fiore, Ohad Kammar, Georg Moser +1
We adapt Fiore, Plotkin, and Turi's treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include pr…
Coverage Semantics for Dependent Pattern Matching
Joseph Eremondi, Ohad Kammar
Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching…
Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics
Yotam Dvir, Ohad Kammar, Ori Lahav +1
We use a two sorted equational theory of algebraic effects to model concurrent shared state with preemptive interleaving, recovering Brookes's seminal 1996 trace-based model precis…
Relaxed exception semantics for Arm-A (extended version)
Ben Simner, Alasdair Armstrong, Thomas Bauereiss +4
To manage exceptions, software relies on a key architectural guarantee, precision: that exceptions appear to execute between instructions. However, this definition, dating back ove…
Modular probabilistic programming with algebraic effects (MSc Thesis 2019)
Oliver Goldstein, Ohad Kammar
Probabilistic programming languages, which exist in abundance, are languages that allow users to calculate probability distributions defined by probabilistic programs, by using inf…
Frex: dependently-typed algebraic simplification
Guillaume Allais, Edwin Brady, Nathan Corbyn +2
We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free…
Idris TyRE: a dependently typed regex parser
Ohad Kammar, Katarzyna Marek
Regular expressions -- regexes -- are widely used not only for validating, but also for parsing textual data. Generally, regex parsers output a loose structure, e.g. an unstructure…
A Domain Theory for Statistical Probabilistic Programming
Matthijs Vákár, Ohad Kammar, Sam Staton
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languag…
Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
Ohad Kammar, Dylan McDermott
Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its retur…
Denotational validation of higher-order Bayesian inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár +7
We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inferenc…
A monadic solution to the Cartwright-Felleisen-Wadler conjecture
Ohad Kammar, Dylan McDermott
Given a programming language, can we give a monadic denotational semantics that is stable under language extension? Models containing only a single monad are not stable. Models bas…
A monad for full ground reference cells
Ohad Kammar, Paul B. Levy, Sean K. Moss +1
We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in…
A Convenient Category for Higher-Order Probability Theory
Chris Heunen, Ohad Kammar, Sam Staton +1
Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outsi…
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Yannick Forster, Ohad Kammar, Sam Lindley +1
We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and de…
No value restriction is needed for algebraic effects and handlers
Ohad Kammar, Matija Pretnar
We present a straightforward, sound Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which allows type variable generalisation…
Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
Sam Staton, Hongseok Yang, Chris Heunen +2
We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Ang…
An absolute characterisation of locally determined omega-colimits
Ohad Kammar
Characterising colimiting omega-cocones of projection pairs in terms of least upper bounds of their embeddings and projections is important to the solution of recursive domain equa…