9 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…
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…
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…
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…
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…