Domain-Theoretic Semantics for Functional Logic Programming
Abstract
Functional Logic Programming (FLP) is a paradigm that extends higher-order functional programming with nondeterministic choice, logical variables, and equational constraints. Starting from the observation that these constructs can be presented as algebraic effects, we rationally reconstruct a core calculus for FLP that is based on call-by-push-value, and supports higher-order functions and recursion. We show how to execute its programs through an abstract machine that implements narrowing. Finally, we present a domain-theoretic semantics based on the lower powerdomain, which we prove to be sound, adequate, and fully abstract with respect to the machine. This leads to an exploration of the limitations of domain theory in modelling FLP.
Fields of Study & Subjects
Logic
Reasoning
and Knowledge
programming
and type systems
Formal Methods in Verification
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Volume
- 10
- Issue
- POPL
- Pages
- 1641–1672
- Publication date
- 8 January 2026
- Language
- EN