The Verse Calculus: a Core Calculus for Functional Logic Programming
Lambda the Ultimate - Programming Languages Weblog 2022-12-13
Summary:
https://simon.peytonjones.org/assets/pdfs/verse-conf.pdf
- LENNART AUGUSTSSON, Epic Games, Sweden
- JOACHIM BREITNER
- KOEN CLAESSEN, Epic Games, Sweden
- RANJIT JHALA, Epic Games, USA
- SIMON PEYTON JONES, Epic Games, United Kingdom
- OLIN SHIVERS, Epic Games, USA/li>
- TIM SWEENEY, Epic Games, USA
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 functional logical 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.
This draft paper describes our current thinking about Verse. It is very much a work in progress, not a finished product. The broad outlines of the design are stable. However, the details of the rewrite rules may well change; we think that the current rules are not confluent, in tiresome ways. (If you are knowledgeable about confluence proofs, please talk to us!)We are eager to enagage in a dialogue with the community. Please do write to us.