The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming
Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele, Tim Sweeney
Abstract
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.
Topics & Concepts
Calculus (dental)Church encodingSimply typed lambda calculusSemantics (computer science)Computer scienceProgramming languageTyped lambda calculusLambda calculusCore (optical fiber)Functional programmingMathematicsMedicineTelecommunicationsDentistryLogic, programming, and type systemsLogic, Reasoning, and KnowledgeFormal Methods in Verification