Constraint Handling Rules (CHR) is a declarative committed-choice programming language with a strong relationship to linear logic. Its generalization CHR with Disjunction (CHRv) is a multi-paradigm declarative programming language that allows the embedding of horn programs. We analyse the assets and the limitations of the classical declarative semantics of CHR before we motivate and develop a linear-logic declarative semantics for CHR and CHRv. We show how to apply the linear-logic semantics to decide program properties and to prove operational equivalence of CHRv programs across the boundaries of language paradigms.
The linear-logic programming language LolliMon, proposed in @cite_10 , integrates backward-chaining proof search with committed-choice forward reasoning. It is an extension of the aforementioned language Lolli. The sequent calculus underlying Lolli extended by a set of dedicated inference rules. The corresponding connectives are syntactically detached from Lolli's own connectives and operationally they are processed within a monad. The actual committed-choice behaviour comes by the explicit statement in the operational semantics, that these inference are to be applied in a committed-choice manner during proof search. With respect to Lolli, committed comes thus comes at the cost of giving up the general notion of execution as proof search, although it is retained outside the monad.
@cite_10
1963779317
Lolli is a logic programming language based on the asynchronous propositions of intuitionistic linear logic. It uses a backward chaining, backtracking operational semantics. In this paper we extend Lolli with the remaining connectives of intuitionistic linear logic restricted to occur inside a monad, an idea taken from the concurrent logical framework (CLF). The resulting language, called LolliMon, has a natural forward chaining, committed choice operational semantics inside the monad, while retaining Lolli's semantics outside the monad. LolliMon thereby cleanly integrates both concurrency and saturation with logic programming search. We illustrate its expressive power through several examples including an implementation of the pi-calculus, a call-by-need lambda-calculus, and several saturating algorithms presented in logical form.