Domain-Theoretic Semantics for Functional Logic Programming

Eddie Jones; Samson S Main; Celia Li; Jonathan Marriott; G. A. Kavvos

doi:10.1145/3776699

Domain-Theoretic Semantics for Functional Logic Programming

Eddie Jones, Samson S Main, Celia Li, Jonathan Marriott, G. A. Kavvos

Research output: Contribution to journal › Article (Academic Journal) › peer-review

5 Downloads (Pure)

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.

Original language	English
Article number	57
Pages (from-to)	1641-1672
Number of pages	32
Journal	Proceedings of the ACM on Programming Languages
Volume	10
Issue number	POPL
DOIs	https://doi.org/10.1145/3776699
Publication status	Published - 8 Jan 2026
Event	53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026) - Rennes, France Duration: 11 Jan 2026 → 17 Jan 2026 https://popl26.sigplan.org/

Bibliographical note

Publisher Copyright:
© 2026 Owner/Author.

Research Groups and Themes

Programming Languages

Keywords

functional logic programming
denotational semantics
domain theory
narrowing
algebraic effects

Access to Document

10.1145/3776699Licence: CC BY

Full-text PDF (final published version) Final published version, 918 KBLicence: CC BY

Handle.net

Persistent link

1 Active
2 Finished

Towards Concurrent Classical Effects
Kavvos, A. (Principal Investigator)
1/12/23 → 31/05/26
Project: Research
Two-dimensional Kripke Semantics and World Models
Kavvos, A. (Principal Investigator)
15/09/24 → 14/09/25
Project: Research
Language Embeddings for Proof Engineering
Kavvos, A. (Principal Investigator)
1/12/23 → 30/11/25
Project: Research

Cite this

@article{3bdffb28464f4335a77ec3a47bb02332,

title = "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.",

keywords = "functional logic programming, denotational semantics, domain theory, narrowing, algebraic effects",

author = "Eddie Jones and Main, \{Samson S\} and Celia Li and Jonathan Marriott and Kavvos, \{G. A.\}",

note = "Publisher Copyright: {\textcopyright} 2026 Owner/Author.; 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026), POPL 2026 ; Conference date: 11-01-2026 Through 17-01-2026",

year = "2026",

month = jan,

day = "8",

doi = "10.1145/3776699",

language = "English",

volume = "10",

pages = "1641--1672",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "POPL",

url = "https://popl26.sigplan.org/",

}

TY - JOUR

T1 - Domain-Theoretic Semantics for Functional Logic Programming

AU - Jones, Eddie

AU - Main, Samson S

AU - Li, Celia

AU - Marriott, Jonathan

AU - Kavvos, G. A.

PY - 2026/1/8

Y1 - 2026/1/8

N2 - 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.

AB - 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.

KW - functional logic programming

KW - denotational semantics

KW - domain theory

KW - narrowing

KW - algebraic effects

U2 - 10.1145/3776699

DO - 10.1145/3776699

M3 - Article (Academic Journal)

SN - 2475-1421

VL - 10

SP - 1641

EP - 1672

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 57

T2 - 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026)

Y2 - 11 January 2026 through 17 January 2026

ER -

Domain-Theoretic Semantics for Functional Logic Programming

Abstract

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Projects

Towards Concurrent Classical Effects

Two-dimensional Kripke Semantics and World Models

Language Embeddings for Proof Engineering

Cite this