The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming
Open Access
- 30 August 2023
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 7 (ICFP) , 417-447
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.Keywords
This publication has 41 references indexed in Scilit:
- On the correctness of pull-tabbingTheory and Practice of Logic Programming, 2011
- Operational semantics for declarative multi-paradigm languagesJournal of Symbolic Computation, 2005
- Skew confluence and the lambda calculus with letrecAnnals of Pure and Applied Logic, 2002
- An approach to declarative programming based on a rewriting logicThe Journal of Logic Programming, 1999
- GOFFIN: Higher-order functions meet concurrent constraintsScience of Computer Programming, 1998
- Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machineJournal of Functional Programming, 1992
- What you always wanted to know about Datalog (and never dared to ask)IEEE Transactions on Knowledge and Data Engineering, 1989
- Generators in IconACM Transactions on Programming Languages and Systems, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- The icon programming languageACM SIGPLAN Notices, 1979