Functional logic languages have a rich literature, but it is tricky to give them a satisfying semantics. In this paper 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.

@article{paperbot1906,
  title = {The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming},
  author = {Lennart Augustsson and Joachim Breitner and Koen Claessen and Ranjit Jhala and Simon Peyton Jones and Olin Shivers and Guy L. Steele Jr. and Tim Sweeney},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {ICFP},
  year = {2023},
  doi = {10.1145/3607845}
}