An instance of FreeCHR with refined operational semantics

Sascha Rechenberger; Thom Fr\"uhwirth

REVIEW 3 major objections 4 minor 1 cited by

An instance of FreeCHR with refined operational semantics

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper proves a new FreeCHR execution algorithm, derived from CHR's refined operational semantics, is sound with respect to FreeCHR's very abstract semantics.

desk verdict Real step toward an implementable FreeCHR, but Theorem 1 needs a distinctness condition on matched store indices before it can be believed. read the letter →

arxiv 2505.22155 v1 pith:4M4YMIUX submitted 2025-05-28 cs.PL

Sascha Rechenberger , Thom Frühwirth This is my paper

classification cs.PL

keywords constrainthandlingrulesFreeCHRrefinedoperationalsemanticsveryabstractinitialalgebraembeddeddomain-specificlanguagessoundnesslabelledtransitionsystems

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

FreeCHR is an algebraic framework for embedding Constraint Handling Rules (CHR) into host languages as libraries, and this paper adds the piece it was missing: a concrete execution algorithm. The algorithm implements the refined operational semantics of CHR, the deterministic version that actual CHR systems use, and the paper's main theorem proves that every step the algorithm takes corresponds to a step of FreeCHR's very abstract semantics once indices and activation bookkeeping are erased. If the theorem holds, implementers get a single provably sound blueprint for building CHR embeddings as internal libraries, and the theory community gets an algorithmic, checkable definition of the refined semantics for FreeCHR. The scope is the ground, positive, range-restricted segment of CHR, and the paper is explicit that completeness and a structural formalization of the refined semantics remain future work.

What carries the argument

The machinery is the FreeCHR instance whose states are quadruples $(\mathit{query}, \mathit{store}, \mathit{history}, \mathit{index})$: a call-stack-like query of values (each either unactivated or carrying a unique index), a store of indexed values, a propagation history of rule-configuration records that prevents repeated firing, and a counter that issues fresh indices. Four algorithms — match, rule, compose, run — implement the refined-semantics behavior: values are activated on entry, tried against head patterns right-to-left and against rules top-to-bottom, fire only when the guard holds and the configuration is not already in the history, and are dropped when no rule applies. Carrying the soundness argument is the catamorphism $\llbracket\mathit{rule}, \mathit{compose}\rrbracket$, which interprets the free-algebra syntax of FreeCHR programs, together with the abstraction function $abstract_r$ that erases decoration to produce the multisets on which the very abstract semantics operates.

What would settle it

Set up a store containing a single value $c$ and a rule with two head patterns that both accept $c$ and a guard that passes; if Algorithm 1 then returns a configuration using the same index twice for the two patterns and Algorithm 2 fires, the abstracted transition would require the abstract apply rule to remove two distinct values from a multiset with only one copy of $c$, which is impossible — such a firing would refute Theorem 1.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: the very abstract semantics $\omega^\star_a$ is abstract_r-sound with respect to the new instance transition system $\omega^\star_r$. Concretely, for any program $p$ and refined states $s,s'$, if the execution algorithm (the functions rule, compose, and run) transforms $s$ into $s'$, then applying the abstraction function $abstract_r$, which maps a refined state to the multiset of store values plus not-yet-activated query values, yields a valid transition (or reflexive chain of transitions) of $\omega^\star_a$ for the same program. The proof is by induction on the structure of the program, and its key case builds an apply transition of the abstract semantics from a successful match of the algorithm, using the guard satisfaction, the removal of matched values, and the addition of body values exactly as the abstract apply rule requires. The paper further claims this constitutes the first formalization of a fully expressive CHR embedding for which there are formal correctness proofs.

Load-bearing premise

The load-bearing assumption is that Algorithm 1 only pairs distinct head patterns with distinct store entries, since the abstract apply rule requires a unique value per pattern; the algorithm never checks that the indices in the matching tuple are pairwise different, and the soundness proof's apply case would collapse without that distinctness.

Editorial extensions

If this is right

Implementations following Algorithms 1-4 are valid concretizations of FreeCHR's very abstract semantics, so correctness properties proved on the abstract model carry over to running systems.
The algorithm gives an algorithmic definition of the refined operational semantics for FreeCHR, giving formal work a concrete, checkable artifact instead of only inference rules.
New CHR embeddings can be built as internal host-language libraries from one proven baseline, eliminating the separate precompiler that external embeddings require.
The algorithm resets the active value's pattern index after each rule application; the paper argues this deviation from the original refined semantics is harmless because the propagation history already prevents re-firing the same configuration.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural testable extension is to prove completeness in addition to soundness: whether every sequence of abstract apply steps can be realized as a run of the algorithm, a question the paper explicitly leaves open.
Closing the distinctness gap is straightforward: changing Algorithm 1's inner loop to reject tuples with repeated indices would make the apply case of the soundness proof airtight, and would likely require only a small amendment to the algorithm text.
The same algebraic-embedding strategy could be tried on other declarative rule-based EDSLs whose implementations outpace their formal semantics, though whether the soundness proof transfers depends on the host language's semantics.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The short version: this is a genuinely useful paper with a hole in its main theorem. Algorithm 1's matching procedure never requires the indices it selects for different head patterns to be pairwise distinct, and the proof of Theorem 1 just assumes it. That assumption is load-bearing. The abstract apply rule needs one distinct store occurrence per head pattern, and the proof's rewrite of abstract_r(s) as {c1,...,c_{n+m}} ⊎ ΔS silently supplies that distinctness. The stress-test note is right about this. With a rule whose two head patterns both match the same store element—say two copies of λx.x=a—Algorithm 1 can return the same (index, value) pair for both positions, and then Algorithm 2 removes an occurrence that was also supposed to be kept. No valid abstract apply step exists. As written, Theorem 1 is unproved and the algorithm is unsound for programs with repeated or overlapping head patterns.

The fix is small and the surrounding work is solid. FreeCHR's use of initial algebra semantics as a common formal backbone for CHR embeddings is a sensible direction, and this paper takes it from an abstract semantics to something an implementor can code against. The algorithm is easy to follow, the GCD and transitive-hull examples are instructive, and the paper is honest about scope: Section 9 admits the ground/range-restricted fragment, the absence of optimizations, and that the GitLab implementations use a DFS/backtracking matcher that is not yet proven equivalent to Algorithm 1. The induction in Section 7 is well structured, and most cases check out—the dead-value popping cases correctly argue that abstract_r is unaffected.

Minor points: ⊑ is never defined, which is exactly the source of the duplicate-index problem; the paper should define it (e.g., as a selection of distinct store elements) and make the distinctness condition explicit. And the abstract's claim of providing 'an algorithmic definition of the refined operational semantics' is stronger than what is shown—soundness is only against the very abstract semantics, and equivalence with the original refined semantics ω_r is deferred to future work. The paper says so in Section 10, but the abstract overstates it.

Audience: CHR implementors and people working on rule-based DSL embeddings; niche, but real. I'd send it to referees, with the expectation of major revision focused on the distinctness gap.

Referee Report

3 major / 4 minor

Summary. The paper introduces an execution algorithm for FreeCHR, an algebraic framework for embedding Constraint Handling Rules (CHR) into host languages. It defines a state space for a refined-style operational semantics, gives four algorithms (matching, single-rule execution, composition, and a driver loop), and proves a soundness theorem relating the algorithmic transition system to the previously defined very abstract semantics of FreeCHR. The paper also claims that the algorithm constitutes an algorithmic definition of the refined operational semantics and provides a practical blueprint for CHR implementations.

Significance. If the technical gaps are repaired, the intended contribution is useful: it connects a concrete, implementable execution strategy for FreeCHR to the framework's abstract semantics, and it provides illustrative examples plus an available implementation. The proof is structured and most of the case analysis is explicit. However, the central soundness theorem currently relies on an unstated distinctness assumption, the theorem statement reverses the soundness direction, and the claim of being 'an algorithmic definition of the refined operational semantics' goes beyond what is proved in the paper.

major comments (3)

[Section 6, Algorithm 1, line 4] The relation `⊑` is never defined, and the enumeration does not require the selected indices `i1,...,in` to be pairwise distinct, nor does it require `i_a` to be distinct from the other selected indices. Consequently, with a rule such as `r@ p, p ==> q` and a store containing only `{(1,a)}`, the tuple `((1,a),(1,a))` can be returned as a match. The abstract apply rule in Definition 3 requires the precondition multiset `{c1,...,c_{n+m}} ⊎ ΔS`; a single store occurrence cannot supply multiplicity two. The proof of Theorem 1 in Section 7 (return-in-Line-20 case) rewrites `abstract_r(s)` as `{c1,...,c_{n+m}} ⊎ ΔS` based on Line 4 of Algorithm 1, so the proof silently assumes that the matched indices are distinct. The algorithm and proof need an explicit injectivity condition on the selected indices, and the notation `⊑` needs a precise definition.
[Section 7, Theorem 1] The theorem is stated as 'ω^★_a is abstract_r-sound with respect to ω^★_r', but this is ill-typed under Definition 2.3 because `abstract_r` maps from `Ω_r C` to `mset C`, while f-soundness in Definition 2.3 requires a function from the first system's states to the second system's states. The proof actually establishes the opposite direction: every transition of `ω^★_r` maps via `abstract_r` to a transition of `ω^★_a`. The theorem statement should be corrected to 'ω^★_r is abstract_r-sound with respect to ω^★_a', and the surrounding text and conclusion should be aligned with that statement.
[Abstract and Section 11] The paper claims to provide 'an algorithmic definition of the refined operational semantics', but Section 10 states that formalizing `ω^★_r` and proving soundness and completeness with respect to the original `ω_r` is future work. Section 6 also explicitly notes that Algorithms 2 and 3 deviate from the original `ω_r` by resetting the pattern index to 1 after a rule application. The only theorem proved is soundness with respect to the very abstract semantics `ω^★_a`. The claim should therefore be weakened to 'an execution algorithm derived from the refined operational semantics and sound with respect to the very abstract semantics', or the missing correspondence proof with `ω_r` must be supplied.

minor comments (4)

[Section 5, Figure 5] The function `activate_C` is declared with type `Ω_r C → N×Ω_r C`, but its defining equation has an additional parameter `c`. The signature or the definition should be adjusted so that they match.
[Section 5, Definition 7] The sentence 'The function in Definition 7 define operations on the propagation history' should refer to Figure 6 and should use singular 'defines'.
[Section 7, proof of the base case] In the return-in-Line-3 case, the sentence 'the only change to the state might have occurred in Line 7' overlooks a possible activation in Line 5. The conclusion still holds because activation leaves `abstract_r` unchanged, but the case analysis should mention this explicitly.
[Section 6, Example 7] The name `substract` appears to be a typo for `subtract` in the definition of `gcd`.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 1 is a direct simulation proof against the separately stated abstract semantics of Definition 3; the self-citations to FreeCHR [27] supply prior definitions, not the target result.

full rationale

The paper's central derivation is Theorem 1, which claims that each transition of the instance transition system ω_r^* (Definition 12, built from Algorithms 1-4) is matched by a transition of the very abstract semantics ω_a^* (Definition 3). Definition 3 restates the abstract semantics from the authors' prior FreeCHR paper inside this manuscript, so the target relation is explicit and is not secretly defined by the algorithm. The proof is an induction over the program structure; in the apply case it uses the guard/pattern checks of Algorithm 1 to construct an instance of the abstract apply rule and rewrites abstract_r(s) into the required multiset form. There are no fitted parameters, no quantity is 'predicted' from data used to define it, and no uniqueness theorem is imported from the authors' prior work to rule out alternatives. The citations to [27] are for the FreeCHR syntax and the original abstract semantics; those are prior formal definitions, not an unverified premise that is equivalent to the new algorithm, so they do not make the derivation circular. The paper itself flags the remaining obligations: Section 10 defers a structural formalization of ω_r^* and a proof of soundness and completeness against the original refined semantics, and Section 9.3 defers a correctness proof of the implemented depth-first-search matcher relative to Algorithm 1; these are honest limitations, not circular moves. There is a real proof gap that is nevertheless not circular: Algorithm 1 iterates over tuples '⊑ store' without requiring the selected indices to be pairwise distinct, and the proof of Theorem 1 rewrites 'abstract_r(s)' as '{c1,...,c_{n+m}} ⊎ Δs' from a mere subset statement, silently assuming the multiplicity that distinct indices would provide. That threatens soundness for repeated head patterns, but it is a correctness defect in the proof, not an equivalence-by-construction, and it does not change the circularity score.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claim depends on prior FreeCHR results by the same authors, a restriction to ground and range-restricted CHR, and assumed correctness of host-language evaluations. No fitted numeric parameters appear.

assumptions (4)

domain assumption FreeCHR's very abstract operational semantics ω_a^★ is a valid representation of classical CHR.
Cited to prior work [27] in Section 4; the current soundness proof builds on this without re-proving it.
domain assumption The ground, positive, range-restricted segment of CHR covers the intended use cases.
Section 9.1 explicitly restricts FreeCHR to this subset, excluding logical variables and failing computations.
domain assumption Host-language evaluation of expressions in patterns, guards, and bodies is correct and total for ground values.
Definition 1 assumes ground evaluated rule instances; the proof relies on these evaluations when checking head and guard conditions.
standard math Standard set-theoretic and inductive reasoning, including structural induction on the free algebra CHR^★_C.
Used throughout Section 7; no machine-checked formalization is provided.

how reviews work

0 comments

Cite this review

Pith. "Pith review of An instance of FreeCHR with refined operational semantics." pith.science (2026). https://pith.science/paper/4M4YMIUX

@misc{pith2026250522155,
  author       = {Pith},
  title        = {Pith review of: An instance of FreeCHR with refined operational semantics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4M4YMIUX}},
  note         = {Machine review of arXiv:2505.22155}
}

read the original abstract

Constraint Handling Rules (CHR) is a rule-based programming language which is typically embedded into a general-purpose language. There exists a plethora of implementations of CHR for numerous host languages. However, the existing implementations often reinvent the way to embed CHR, which impedes maintenance and weakens assertions of correctness. To formalize and thereby unify the embedding of CHR into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical CHR. Until now, this framework only includes a translation of the very abstract operational semantics of CHR which, due to its abstract nature, introduces several practical issues. In this paper, we introduce an execution algorithm for FreeCHR. We derive it from the refined operational semantics of CHR, which resolve the issues introduced by the very abstract semantics. We also prove soundness of the algorithm with respect to the very abstract semantics of FreeCHR. Hereby we provide a unified and an easy to implement guideline for new CHR implementations, as well as an algorithmic definition of the refined operational semantics.

Figures

Figures reproduced from arXiv: 2505.22155 by the authors.

**Figure 2.** Demonstration of the effect of the propagation history. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 5.** Operations on the store of a state to_history𝐶 : Ω𝑟𝐶 ×(str × listN) −→ Ω𝑟𝐶 to_history𝐶 (⟨𝑄, 𝑆, 𝐻, 𝐼⟩, 𝑟𝑢𝑙𝑒𝑛𝑎𝑚𝑒,𝑖1, ...,𝑖𝑛) = ⟨𝑄, 𝑆, 𝐻 ∪ {(𝑟𝑢𝑙𝑒𝑛𝑎𝑚𝑒,𝑖1, ...,𝑖𝑛)} , 𝐼⟩ [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗

Figures from the paper (1 more)

**Figure 7.** Figure 7: Execution of the Euclidean algorithm implemented [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Optimized Execution of FreeCHR
cs.PL 2025-06 reject novelty 4.0 of 10

An improved FreeCHR execution algorithm with iterator-based matching and manual indexing is presented and benchmarked, but correctness is unproven and the measured gains are mixed.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages · cited by 1 Pith paper

[1]

JACK: A Java Constraint Kit

Slim Abdennadher, Ekkerhard Krämer, Matthias Saft, and Matthias Schmauss. JACK: A Java Constraint Kit. InElectronic Notes in Theoretical Computer Science, volume 64, pages 1–17, 2002

work page 2002
[2]

University course timetabling using constraint handling rules

Slim Abdennadher and Michael Marte. University course timetabling using constraint handling rules. volume 14, pages 311–325, April 2000

work page 2000
[3]

CHR++: An efficient CHR system in C++ with don’t know non-determinism

Vincent Barichard. CHR++: An efficient CHR system in C++ with don’t know non-determinism. volume 238, page 121810, March 2024

work page 2024
[4]

Byrd.Relational Programming in miniKanren: Techniques, Applications, and Implementations

William E. Byrd.Relational Programming in miniKanren: Techniques, Applications, and Implementations. PhD thesis, Indiana University, United States – Indiana, 2009

work page 2009
[5]

Finally Tagless, Partially Evaluated

Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. Finally Tagless, Partially Evaluated. In Zhong Shao, editor,APLAS 07, Lecture Notes in Computer Science, pages 222–238, Berlin, Heidelberg, 2007. Springer

work page 2007
[6]

W. Chin, M. Sulzmann, and Meng Wang. A Type-Safe Embedding of Constraint Handling Rules into Haskell. 2008

work page 2008
[7]

Henning Christiansen and Maja H. Kirkeby. Confluence Modulo Equivalence in Constraint Handling Rules. In Maurizio Proietti and Hirohisa Seki, editors, Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science, pages 41–58, Cham, 2015. Springer International Publishing

work page 2015
[8]

Leslie De Koninck, Tom Schrijvers, Bart Demoen, M. Fink, H. Tompits, and S. Woltran. INCLP(R) - Interval-based nonlinear constraint logic programming over the reals. InWLP ’06, volume 1843-06-02. Technische Universität Wien, Austria, January 2006

work page 2006

Show all 37 references

[9]

PhD thesis, University of Melbourne, Victoria, Australia, 2005

Gregory J Duck.Compilation of Constraint Handling Rules. PhD thesis, University of Melbourne, Victoria, Australia, 2005

2005
[10]

Duck, Peter J

Gregory J. Duck, Peter J. Stuckey, María García de la Banda, and Christian Holzbaur. The Refined Operational Semantics of Constraint Handling Rules. In Bart Demoen and Vladimir Lifschitz, editors,ICLP ’04, Lecture Notes in Computer Science, pages 90–104, Berlin, Heidelberg, 20...

2004
[11]

Complete Propagation Rules for Lexicographic Order Con- straints over Arbitrary Domains

Thom Frühwirth. Complete Propagation Rules for Lexicographic Order Con- straints over Arbitrary Domains. In Brahim Hnich, Mats Carlsson, François Fages, and Francesca Rossi, editors,CSCLP ’05, Lecture Notes in Computer Science, pages 14–28, Berlin, Heidelberg, 2006. Springer

2006
[12]

Cambridge University Press, Cam- bridge, U.K

Thom Frühwirth.Constraint Handling Rules. Cambridge University Press, Cam- bridge, U.K. New York, 2009

2009
[13]

Thom Frühwirth. Constraint Handling Rules - What Else? In Nick Bassili- ades, Georg Gottlob, Fariba Sadri, Adrian Paschke, and Dumitru Roman, edi- tors,RuleML ’15, Lecture Notes in Computer Science, pages 13–34, Cham, 2015. Springer International Publishing. An instance of Fre...

2015
[14]

BoD, ISBN 978-3-7693- 7633-3, 2025

Thom Frühwirth.Principles of Rule-Based Programming. BoD, ISBN 978-3-7693- 7633-3, 2025

2025
[15]

A Decidable Confluence Test for Cognitive Models in ACT-R

Daniel Gall and Thom Frühwirth. A Decidable Confluence Test for Cognitive Models in ACT-R. In Stefania Costantini, Enrico Franconi, William Van Woensel, Roman Kontchakov, Fariba Sadri, and Dumitru Roman, editors,Rules and Rea- soning, pages 119–134, Cham, 2017. Springer Intern...

2017
[16]

CHR(Curry): Interpretation and Compilation of Constraint Handling Rules in Curry

Michael Hanus. CHR(Curry): Interpretation and Compilation of Constraint Handling Rules in Curry. In Enrico Pontelli and Tran Cao Son, editors,PADL ’15, Lecture Notes in Computer Science, pages 74–89, Cham, 2015. Springer International Publishing

2015
[17]

Modular domain-specific language com- ponents in scala

Christian Hofer and Klaus Ostermann. Modular domain-specific language com- ponents in scala. InGPCE ’10. ACM Press, 2010

2010
[18]

Poly- morphic embedding of dsls

Christian Hofer, Klaus Ostermann, Tillmann Rendel, and Adriaan Moors. Poly- morphic embedding of dsls. InGPCE ’08. ACM Press, 2008

2008
[19]

Compiling Constraint Handling Rules

Christian Holzbaur and Thom Frühwirth. Compiling Constraint Handling Rules. InERCIM/COMPULOG Workshop on Constraints, Amsterdam, 1998

1998
[20]

A prolog constraint handling rules compiler and runtime system

Christian Holzbaur and Thom Frühwirth. A prolog constraint handling rules compiler and runtime system. volume 14, pages 369–388. Taylor & Francis, April 2000

2000
[21]

P. Hudak. Modular domain specific languages and tools. InICSR ’98, pages 134–142, June 1998

1998
[22]

Implementing Constraint Handling Rules as a Domain-Specific Language Embedded in Java, August 2013

Dragan Ivanović. Implementing Constraint Handling Rules as a Domain-Specific Language Embedded in Java, August 2013

2013
[23]

Initial Algebra Semantics Is Enough! In Si- mona Ronchi Della Rocca, editor,TLCA ’07, Lecture Notes in Computer Science, pages 207–222, Berlin, Heidelberg, 2007

Patricia Johann and Neil Ghani. Initial Algebra Semantics Is Enough! In Si- mona Ronchi Della Rocca, editor,TLCA ’07, Lecture Notes in Computer Science, pages 207–222, Berlin, Heidelberg, 2007. Springer

2007
[24]

Lam and Martin Sulzmann

E. Lam and Martin Sulzmann. Towards Agent Programming in CHR. 2006

2006
[25]

Edmund S. L. Lam and Martin Sulzmann. A concurrent constraint handling rules implementation in Haskell with software transactional memory. InDAMP ’07, pages 19–24, Nice, France, 2007. ACM Press

2007
[26]

CHR.js: A CHR Implementa- tion in JavaScript

Falco Nogatz, Thom Frühwirth, and Dietmar Seipel. CHR.js: A CHR Implementa- tion in JavaScript. In Christoph Benzmüller, Francesco Ricca, Xavier Parent, and Dumitru Roman, editors,RuleML ’18, Lecture Notes in Computer Science, pages 131–146, Cham, 2018. Springer International ...

2018
[27]

FreeCHR: An Algebraic Framework for CHR-Embeddings

Sascha Rechenberger and Thom Frühwirth. FreeCHR: An Algebraic Framework for CHR-Embeddings. In Anna Fensel, Ana Ozaki, Dumitru Roman, and Ahmet Soylu, editors,RuleML+RR ’23, Lecture Notes in Computer Science, pages 190–205, Cham, 2023. Springer Nature Switzerland

2023
[28]

Certified Seman- tics for Relational Programming

Dmitry Rozplokhas, Andrey Vyatkin, and Dmitry Boulytchev. Certified Seman- tics for Relational Programming. In Bruno C. d. S. Oliveira, editor,Programming Languages and Systems, pages 167–185, Cham, 2020. Springer International Pub- lishing

2020
[29]

Tom Schrijvers and Bart Demoen. The K.U. Leuven CHR system: Implementation and application. InCHR ’04, pages 1–5, 2004

2004
[30]

As time goes by: Constraint Handling Rules: A survey of CHR research from 1998 to 2007

Jon Sneyers, Peter van Weert, Tom Schrijvers, and Leslie De Koninck. As time goes by: Constraint Handling Rules: A survey of CHR research from 1998 to 2007. volume 10, pages 1–47. Cambridge University Press, January 2010

1998
[31]

Reasoning about Actions with CHRs and Finite Domain Constraints

Michael Thielscher. Reasoning about Actions with CHRs and Finite Domain Constraints. In Peter J. Stuckey, editor,LP ’02, Lecture Notes in Computer Science, pages 70–84, Berlin, Heidelberg, 2002. Springer

2002
[32]

FLUX: A logic programming method for reasoning agents

Michael Thielscher. FLUX: A logic programming method for reasoning agents. volume 5, pages 533–565, July 2005

2005
[33]

Efficient Lazy Evaluation of Rule-Based Programs

Peter van Weert. Efficient Lazy Evaluation of Rule-Based Programs. volume 22, pages 1521–1534, November 2010

2010
[34]

Peter van Weert, Tom Schrijvers, Bart Demoen, Tom Schrijvers, and Thom Früh- wirth. K.U. Leuven JCHR: A user-friendly, flexible and efficient CHR system for Java. InCHR ’05. Deptartment of Computer Science, K.U.Leuven, 2005

2005
[35]

CHR for Imperative Host Languages

Peter van Weert, Pieter Wuille, Tom Schrijvers, and Bart Demoen. CHR for Imperative Host Languages. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules: Current Research Topics, Lecture Notes in Computer Science, pages 161–212, Berlin, Heidelberg, 2008. Springer

2008
[36]

Bachelor thesis, Universität Ulm, June 2022

Tim Wibiral.JavaCHR – A Modern CHR-Embedding in Java. Bachelor thesis, Universität Ulm, June 2022

2022
[37]

CCHR: The fastest CHR Imple- mentation, in C

Pieter Wuille, Tom Schrijvers, and Bart Demoen. CCHR: The fastest CHR Imple- mentation, in C. InCHR ’07, pages 123–137, 2007

2007

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

JACK: A Java Constraint Kit

Slim Abdennadher, Ekkerhard Krämer, Matthias Saft, and Matthias Schmauss. JACK: A Java Constraint Kit. InElectronic Notes in Theoretical Computer Science, volume 64, pages 1–17, 2002

work page 2002

[2] [2]

University course timetabling using constraint handling rules

Slim Abdennadher and Michael Marte. University course timetabling using constraint handling rules. volume 14, pages 311–325, April 2000

work page 2000

[3] [3]

CHR++: An efficient CHR system in C++ with don’t know non-determinism

Vincent Barichard. CHR++: An efficient CHR system in C++ with don’t know non-determinism. volume 238, page 121810, March 2024

work page 2024

[4] [4]

Byrd.Relational Programming in miniKanren: Techniques, Applications, and Implementations

William E. Byrd.Relational Programming in miniKanren: Techniques, Applications, and Implementations. PhD thesis, Indiana University, United States – Indiana, 2009

work page 2009

[5] [5]

Finally Tagless, Partially Evaluated

Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. Finally Tagless, Partially Evaluated. In Zhong Shao, editor,APLAS 07, Lecture Notes in Computer Science, pages 222–238, Berlin, Heidelberg, 2007. Springer

work page 2007

[6] [6]

W. Chin, M. Sulzmann, and Meng Wang. A Type-Safe Embedding of Constraint Handling Rules into Haskell. 2008

work page 2008

[7] [7]

Henning Christiansen and Maja H. Kirkeby. Confluence Modulo Equivalence in Constraint Handling Rules. In Maurizio Proietti and Hirohisa Seki, editors, Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science, pages 41–58, Cham, 2015. Springer International Publishing

work page 2015

[8] [8]

Leslie De Koninck, Tom Schrijvers, Bart Demoen, M. Fink, H. Tompits, and S. Woltran. INCLP(R) - Interval-based nonlinear constraint logic programming over the reals. InWLP ’06, volume 1843-06-02. Technische Universität Wien, Austria, January 2006

work page 2006