“Functional logic languages have a rich literature, but it is tricky to give them a satisfying semantics. … We describe the Verse calculus, VC, a new core calculus for deterministic functional logic programming. Our main contribution is to equip VC with a small-step rewrite semantics, so that we can reason about a VC program in the same way as one does with lambda calculus; that is, by applying successive rewrites to it. We also show that the rewrite system is confluent for well-behaved terms.”

Find the article and authors list in the Proceedings of the ACM on Programming Languages.