The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi...
summary
A new core calculus (VC) gives a small-step rewrite semantics for a deterministic functional logic language and implements unification and logical variables as plain rewrite rules, including an explicit unification-by-rewrite substitution rule and tuple decomposition that reduce equations to concrete values in examples. Choice is reified as ordered arrays so nondeterministic results are sequences, and the calculus uses a context-duplication rule for choice. The paper proves confluence for a restricted fragment, ships a usable subset now, and is working on a skew-confluence proof.
AI-written summary · about
chapters (8)
- 0:00Introduction to Verse
- 1:03The Metaverse vision
- 2:24The Verse research project
- 5:54Existentials and equations
- 10:22Deterministic choice
- 13:25Rewrite semantics
- 19:00Language mechanics and rules
- 23:32Conclusion and Q&A
related talks
15mStable Relations and Abstract Interpretation of Higher-Order Programs
42mVerse - A New Functional Logic Language
14mDestination calculus: A linear λ-calculus for purely functional memory writes
14mAdequacy for Algebraic Effects Revisited
28mElements of Logic Programming in a Concatenative Functional Language
13mCompiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
01h 02mAnother Taste of Verse
18mOn the Expressive Power of Languages for Static Variability