113 citations · 319 across the 18 of their papers we have counts for
Showing 2025Show all
3 papers · 1 filter
cs.PL2025
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…
cs.PL2025
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…
cs.PL2025★ 2 cited
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…