Denotational Semantics of a Relational λ-Calculus

Mariana Milicich

University of Tartu



Abstract: Functional logic programming is a paradigm that combines features of functional and logic programming, resulting in simpler and more reliable solutions to programming problems. Some examples of the functional logic paradigm are λProlog, Curry, Mercury, and the recent Verse. Nonetheless, providing a denotational semantics for functional logic languages is not trivial, and has only recently gained significant interest.

This talk focuses on the λu-calculus, a functional logic language that extends the λ-calculus with logic programming features: non-deterministic choice, first-order unification, and fresh variable introduction. We provide a type system and formulate a denotational semantics for its typed fragment. We prove, as expected, that this denotational semantics is compositional. Although several discrepancies between the operational and denotational semantics limit full soundness and completeness, this work lays the ground for a more robust understanding of this hybrid paradigm.