Publications of year 2008 (complete with abstract and BibTeX)

Publications of year 2008

Books and proceedings

Tom Schrijvers and Thom Frühwirth, editors. Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8]

@book{lnai08,
editor = {Tom Schrijvers and Thom Fr{\"u}hwirth},
title = {{C}onstraint {H}andling {R}ules --- Current Research Topics},
series = LNAI,
volume = 5388,
year = 2008,
month = dec,
publisher = SV,
doi = {10.1007/978-3-540-92243-8},
url = {http://www.springer.com/computer/artificial/book/978-3-540-92242-1},

}

M. Garcìa de la Banda and E. Pontelli, editors. ICLP '08: Proc. 24rd Intl. Conf. Logic Programming, volume 5366 of Lecture Notes in Computer Science, December 2008. Springer-Verlag. [doi:10.1007/978-3-540-89982-2]

@proceedings{piclp08,
title = ICLP08l,
booktitle = ICLP08,
year = 2008,
month = dec,
location = {Udine, Italy},
city = {Udine, Italy},
editor = {Garc{\'i}a de la Banda, M. and E. Pontelli},
series = LNCS,
volume = 5366,
doi = {10.1007/978-3-540-89982-2},
publisher = SV,

}

M. Hanus, editor. LOPSTR '08: 18th Intl. Symp. Logic-Based Program Synthesis and Transformation, Pre-Proceedings, 2008. [WWW] [PDF]

@proceedings{plopstr08pre,
title = LOPSTR08prel,
booktitle = LOPSTR08pre,
year = 2008,
location = {Valencia, Spain},
city = {Valencia, Spain},
editor = {M. Hanus},
url = {http://www.informatik.uni-kiel.de/~mh/lopstr08/},
pdf = {http://www.informatik.uni-kiel.de/~mh/lopstr08/preproceedings.pdf},

}

A. King, editor. LOPSTR '07: 17th Intl. Symp. Logic-Based Program Synthesis and Transformation, Revised Selected Papers, volume 4915 of Lecture Notes in Computer Science, 2008.

@proceedings{plopstr07,
title = LOPSTR07l,
booktitle = LOPSTR07,
year = 2008,
location = {Kongens Lyngby, Denmark},
city = {Kongens Lyngby, Denmark},
editor = {A. King},
series = LNCS,
volume = 4915,

}

T. Schrijvers, F. Raiser, and T. Frühwirth, editors. CHR '08: Proc. 5th Workshop on Constraint Handling Rules, 2008. RISC Report Series 08-10, University of Linz, Austria. Keyword(s): CHR 2008.

@proceedings{pchr08,
title = CHR08l,
booktitle = CHR08,
year = {2008},
location = {Hagenberg, Austria},
city = {Hagenberg, Austria},
editor = {T. Schrijvers and F. Raiser and T. Fr{\"u}hwirth},
publisher = {RISC Report Series 08-10, University of Linz, Austria},
keywords = {CHR 2008},

}

Thesis

Leslie De Koninck. Execution Control for Constraint Handling Rules. PhD thesis, K.U.Leuven, Belgium, November 2008. [WWW] [PDF] Keyword(s): priorities, complexity, related formalisms. Abstract:

Constraint Programming (CP) is a high-level declarative programming paradigm in which problems are modeled by means of constraints on the problem variables that need to hold in all solutions to the problem. Many problems of high practical relevance can easily be described in terms of constraints. Example application areas include production planning and crew scheduling. A constraint programming system contains a constraint solver whose task it is to find valuations for the problem variables that satisfy all constraints. Constraint programming systems can be classified by the variable domains and types of constraints their solver supports. However, for many problems it is not so straightforward to create a model in terms of basic constraint domains. Therefore, on the one hand, systems emerged that can handle more specialized constraint domains. On the other hand, facilities were designed that make it easier to implement an application-specific constraint solver. Some notable examples of these facilities are attributed variables, and Constraint Handling Rules. Constraint Handling Rules (CHR) is a rule-based language, designed for the implementation of application-specific constraint solvers. CHR is a very flexible language for the specification of a constraint solvers' logic, but flexible execution control is almost completely lacking. Execution control is of great importance for the efficiency of CP systems. However, so far, the problem of execution control has received only very limited attention in the context of CHR. In this thesis, we propose a solution to the problem of execution control in CHR. In particular, we extend CHR with high-level facilities to support the specification of execution strategies. More precisely, we extend CHR with user-defined rule priorities into CHR^rp. CHR rules correspond to constraint propagators, and so rule priorities enable the specification of propagation strategies. An optimized implementation of CHR^rp is presented and evaluated empirically. Next, we extend CHR with facilities for search strategy control. Our approach combines CHR^∨ (CHR with disjunction) and CHR^rp into a new language called CHR_∨^brp in which the propagation strategy is determined by means of rule priorities, and the search strategy by means of branch priorities. We propose a framework for analyzing the time complexity of CHR^rp programs, by combining the Logical Algorithms framework (LA) of Ganzinger and McAllester with CHR^rp. We present translation schemas from and to LA and propose an alternative implementation for CHR^rp with strong complexity guarantees. Finally, we investigate the join order optimization problem, which is an important aspect of optimized CHR compilation. We propose a cost model for matching multi-headed rules, approximations of its parameters, and methods to find an optimal join order. An extension of the model for CHR^rp is given.

@phdthesis{dekoninck_phdthesis08,
author = {De Koninck, Leslie},
title = {Execution Control for {C}onstraint {H}andling {R}ules},
school = {K.U.Leuven},
year = 2008,
address = {Belgium},
month = nov,
abstract = { Constraint Programming (CP) is a high-level declarative programming paradigm in which problems are modeled by means of constraints on the problem variables that need to hold in all solutions to the problem. Many problems of high practical relevance can easily be described in terms of constraints. Example application areas include production planning and crew scheduling. A constraint programming system contains a constraint solver whose task it is to find valuations for the problem variables that satisfy all constraints. 

Constraint programming systems can be classified by the variable domains and types of constraints their solver supports. However, for many problems it is not so straightforward to create a model in terms of basic constraint domains. Therefore, on the one hand, systems emerged that can handle more specialized constraint domains. On the other hand, facilities were designed that make it easier to implement an application-specific constraint solver. Some notable examples of these facilities are attributed variables, and Constraint Handling Rules. 

Constraint Handling Rules (CHR) is a rule-based language, designed for the implementation of application-specific constraint solvers. CHR is a very flexible language for the specification of a constraint solvers' logic, but flexible execution control is almost completely lacking. Execution control is of great importance for the efficiency of CP systems. However, so far, the problem of execution control has received only very limited attention in the context of CHR. In this thesis, we propose a solution to the problem of execution control in CHR. In particular, we extend CHR with high-level facilities to support the specification of execution strategies. 

More precisely, we extend CHR with user-defined rule priorities into CHR$^\mathrm{rp}$. CHR rules correspond to constraint propagators, and so rule priorities enable the specification of propagation strategies. An optimized implementation of CHR$^\mathrm{rp}$ is presented and evaluated empirically. Next, we extend CHR with facilities for search strategy control. Our approach combines CHR$^\vee$ (CHR with disjunction) and CHR$^\mathrm{rp}$ into a new language called CHR$_\vee^\mathrm{brp}$ in which the propagation strategy is determined by means of rule priorities, and the search strategy by means of branch priorities. We propose a framework for analyzing the time complexity of CHR$^\mathrm{rp}$ programs, by combining the Logical Algorithms framework (LA) of Ganzinger and McAllester with CHR$^\mathrm{rp}$. We present translation schemas from and to LA and propose an alternative implementation for CHR$^\mathrm{rp}$ with strong complexity guarantees. Finally, we investigate the join order optimization problem, which is an important aspect of optimized CHR compilation. We propose a cost model for matching multi-headed rules, approximations of its parameters, and methods to find an optimal join order. An extension of the model for CHR$^\mathrm{rp}$ is given. },
keywords = {priorities, complexity, related formalisms},
url = {http://www.cs.kuleuven.be/publicaties/doctoraten/cw/CW2008_13.abs.html},
pdf = {http://www.cs.kuleuven.be/publicaties/doctoraten/cw/CW2008_13.pdf},

}

Mark Meister. Advances in Constraint Handling Rules. PhD thesis, Universität Ulm, Germany, 2008.

@phdthesis{meister_thesis2008,
author = {Mark Meister},
title = {Advances in {C}onstraint {H}andling {R}ules},
school = {Universit{\"a}t Ulm},
address = {Germany},
year = 2008,

}

Jon Sneyers. Optimizing Compilation and Computational Complexity of Constraint Handling Rules. PhD thesis, K.U.Leuven, Belgium, November 2008. [WWW] [PDF] Keyword(s): implementation, optimizing compilation, complexity, computability. Abstract:

Constraint Handling Rules (CHR) is a very-high-level declarative programming language based on concurrent multiset rewrite rules that are conditional, multi-headed, and committed-choice. Originally designed in the early 1990s as a special-purpose programming language for adding user-defined constraint solvers to a host language, CHR has evolved over the last decade into a powerful and elegant general-purpose language with a wide spectrum of application domains. Computational complexity theory is the study of scalability of computer programs in terms of the computational resources they require — in particular, time (cpu usage) and space (memory usage). In this dissertation we investigate the CHR programming language from the point of view of computational complexity theory. The first part introduces complexity theory, CHR, and CHR compilation. In the second part, we improve the state of the art by proposing and implementing several compiler optimizations. We confirm experimentally that these optimizations improve both the time and space complexity of CHR programs. Finally, in the third part of this dissertation, we prove a ``complexity-wise completeness'' result. We demonstrate that the CHR language and state-of-the-art CHR systems (that implement the compiler optimizations of the previous part) are sufficiently efficient in the following precise sense: \emph{every algorithm can be implemented in CHR and be executed with the optimal asymptotic time and space complexity}.

@phdthesis{sneyers_phdthesis08,
author = {Jon Sneyers},
title = {Optimizing Compilation and Computational Complexity of {C}onstraint {H}andling {R}ules},
school = {K.U.Leuven},
year = 2008,
address = {Belgium},
month = nov,
abstract = { Constraint Handling Rules (CHR) is a very-high-level declarative programming language based on concurrent multiset rewrite rules that are conditional, multi-headed, and committed-choice. Originally designed in the early 1990s as a special-purpose programming language for adding user-defined constraint solvers to a host language, CHR has evolved over the last decade into a powerful and elegant general-purpose language with a wide spectrum of application domains. 

Computational complexity theory is the study of scalability of computer programs in terms of the computational resources they require --- in particular, time (cpu usage) and space (memory usage). 

In this dissertation we investigate the CHR programming language from the point of view of computational complexity theory. The first part introduces complexity theory, CHR, and CHR compilation. In the second part, we improve the state of the art by proposing and implementing several compiler optimizations. We confirm experimentally that these optimizations improve both the time and space complexity of CHR programs. 

Finally, in the third part of this dissertation, we prove a ``complexity-wise completeness'' result. We demonstrate that the CHR language and state-of-the-art CHR systems (that implement the compiler optimizations of the previous part) are sufficiently efficient in the following precise sense: \emph{every algorithm can be implemented in CHR and be executed with the optimal asymptotic time and space complexity}. },
keywords = {implementation, optimizing compilation, complexity, computability},
url = {http://www.cs.kuleuven.be/publicaties/doctoraten/cw/CW2008_14.abs.html},
pdf = {http://www.cs.kuleuven.be/publicaties/doctoraten/cw/CW2008_14.pdf},

}

Paolo Tacchella. Constraint Handling Rules — Compositional Semantics and Program Transformation. PhD thesis, Department of Computer Science, University of Bologna, Italy, March 2008. [WWW] [PDF] Keyword(s): semantics. Abstract:

This thesis intends to investigate two aspects of Constraint Handling Rules (CHR). It proposes a compositional semantics and a technique for program transformation. CHR is a concurrent committed-choice constraint logic programming language consisting of guarded rules, which transform multi-sets of atomic formulas (constraints) into simpler ones until exhaustion and it belongs to the declarative languages family. It was initially designed for writing constraint solvers but it has recently also proven to be a general purpose language, being as it is Turing equivalent. Compositionality is the first CHR aspect to be considered. A trace based compositional semantics for CHR was previously defined. The reference operational semantics for such a compositional model was the original operational semantics for CHR which, due to the propagation rule, admits trivial non-termination. In this thesis we extend the above mentioned work by introducing a more refined trace based compositional semantics which also includes the history. The use of history is a well-known technique in CHR which permits us to trace the application of propagation rules and consequently it permits trivial non-termination avoidance. Naturally, the reference operational semantics, of our new compositional one, uses history to avoid trivial non-termination too. Program transformation is the second CHR aspect to be considered, with particular regard to the unfolding technique. Said technique is an appealing approach which allows us to optimize a given program and in more detail to improve run-time efficiency or space-consumption. Essentially it consists of a sequence of syntactic program manipulations which preserve a kind of semantic equivalence called qualified answer, between the original program and the transformed ones. The unfolding technique is one of the basic operations which is used by most program transformation systems. It consists in the replacement of a procedure-call by its definition. In CHR every conjunction of constraints can be considered as a procedure-call, every CHR rule can be considered as a procedure and the body of said rule represents the definition of the call. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. We define an unfolding rule, show its correctness and discuss some conditions in which it can be used to delete an unfolded rule while preserving the meaning of the original program. Finally, confluence and termination maintenance between the original and transformed programs are shown.

@phdthesis{tacchella_thesis2008,
author = {Paolo Tacchella},
title = {{C}onstraint {H}andling {R}ules --- Compositional Semantics and Program Transformation},
school = deptcw # {, University of Bologna},
address = {Italy},
year = 2008,
month = mar,
pdf = {http://amsdottorato.cib.unibo.it/912/1/Tesi_Tacchella_Paolo.pdf},
url = {http://amsdottorato.cib.unibo.it/912/},
abstract = { This thesis intends to investigate two aspects of Constraint Handling Rules (CHR). It proposes a compositional semantics and a technique for program transformation. CHR is a concurrent committed-choice constraint logic programming language consisting of guarded rules, which transform multi-sets of atomic formulas (constraints) into simpler ones until exhaustion and it belongs to the declarative languages family. It was initially designed for writing constraint solvers but it has recently also proven to be a general purpose language, being as it is Turing equivalent. Compositionality is the first CHR aspect to be considered. A trace based compositional semantics for CHR was previously defined. The reference operational semantics for such a compositional model was the original operational semantics for CHR which, due to the propagation rule, admits trivial non-termination. In this thesis we extend the above mentioned work by introducing a more refined trace based compositional semantics which also includes the history. The use of history is a well-known technique in CHR which permits us to trace the application of propagation rules and consequently it permits trivial non-termination avoidance. Naturally, the reference operational semantics, of our new compositional one, uses history to avoid trivial non-termination too. Program transformation is the second CHR aspect to be considered, with particular regard to the unfolding technique. Said technique is an appealing approach which allows us to optimize a given program and in more detail to improve run-time efficiency or space-consumption. Essentially it consists of a sequence of syntactic program manipulations which preserve a kind of semantic equivalence called qualified answer, between the original program and the transformed ones. The unfolding technique is one of the basic operations which is used by most program transformation systems. It consists in the replacement of a procedure-call by its definition. In CHR every conjunction of constraints can be considered as a procedure-call, every CHR rule can be considered as a procedure and the body of said rule represents the definition of the call. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. We define an unfolding rule, show its correctness and discuss some conditions in which it can be used to delete an unfolded rule while preserving the meaning of the original program. Finally, confluence and termination maintenance between the original and transformed programs are shown. },
keywords = {semantics},

}

Articles in journal, book chapters

Bernhard K. Aichernig and He Jifeng. Mutation testing in UTP. Formal Aspects of Computing, 21(1–2):33-64, February 2008. [doi:10.1007/s00165-008-0083-6] Keyword(s): testing. Abstract:

This paper presents a theory of testing that integrates into Hoare and Heâ€™s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.

@article{mutation_testing_fac08,
author = {Bernhard K. Aichernig and He Jifeng},
title = {Mutation testing in {UTP}},
journal = {Formal Aspects of Computing},
publisher = SV,
volume = 21,
number = {1--2},
pages = {33--64},
month = feb,
year = 2008,
doi = {10.1007/s00165-008-0083-6},
keywords = {testing},
abstract = { This paper presents a theory of testing that integrates into Hoare and Heâ€™s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language. },

}

Khalil Djelloul, Dao Thi-Bich-Hanh, and Thom Frühwirth. Theory of finite or infinite trees revisited. Theory and Practice of Logic Programming, 8(4):431-489, 2008. [doi:10.1017/S1471068407003171] Abstract:

We present in this paper a first-order axiomatization of an extended theory $T$ of finite or infinite trees, built on a signature containing an infinite set of function symbols and a relation $finite(t)$, which enables to distinguish between finite and infinite trees. We show that $T$ has at least one model and prove its completeness by giving not only a decision procedure, but a full first-order constraint solver that gives clear and explicit solutions for any first-order constraint satisfaction problem in $T$. The solver is given in the form of 16 rewriting rules that transform any first-order constraint $\Phi$ into an equivalent disjunction $/phi$ of simple formulas such that $\phi$ is either the formula $true$ or the formula $false$ or a formula having at least one free variable, being equivalent neither to $true$ nor to $false$ and where the solutions of the free variables are expressed in a clear and explicit way. The correctness of our rules implies the completeness of $T$. We also describe an implementation of our algorithm in CHR (Constraint Handling Rules) and compare the performance with an implementation in C++ and that of a recent decision procedure for decomposable theories.

@article{djelloul_et_al_trees_revisited_tplp08,
author = {Khalil Djelloul and Dao Thi-Bich-Hanh and Thom Fr{\"u}hwirth},
title = {Theory of finite or infinite trees revisited},
journal = TPLP,
volume = 8,
number = 4,
pages = {431--489},
year = 2008,
publisher = CUP,
abstract = { We present in this paper a first-order axiomatization of an extended theory $T$ of finite or infinite trees, built on a signature containing an infinite set of function symbols and a relation $finite(t)$, which enables to distinguish between finite and infinite trees. We show that $T$ has at least one model and prove its completeness by giving not only a decision procedure, but a full first-order constraint solver that gives clear and explicit solutions for any first-order constraint satisfaction problem in $T$. The solver is given in the form of 16 rewriting rules that transform any first-order constraint $\Phi$ into an equivalent disjunction $/phi$ of simple formulas such that $\phi$ is either the formula $true$ or the formula $false$ or a formula having at least one free variable, being equivalent neither to $true$ nor to $false$ and where the solutions of the free variables are expressed in a clear and explicit way. The correctness of our rules implies the completeness of $T$. We also describe an implementation of our algorithm in CHR (Constraint Handling Rules) and compare the performance with an implementation in C++ and that of a recent decision procedure for decomposable theories. },
doi = {10.1017/S1471068407003171},

}

Tom Schrijvers, Bart Demoen, and David S. Warren. TCHR: a framework for tabled CLP. Theory and Practice of Logic Programming, 8(4):491-526, July 2008. [doi:10.1017/S147106840800327X] Keyword(s): implementation. Abstract:

Tabled Constraint Logic Programming is a powerful execution mechanism for dealing with Constraint Logic Programming without worrying about fixpoint computation. Various applications, e.g. in the fields of program analysis and model checking, have been proposed. Unfortunately, a high-level system for developing new applications is lacking, and programmers are forced to resort to complicated ad hoc solutions. This papers presents TCHR, a high-level framework for tabled Constraint Logic Programming. It integrates in a light-weight manner Constraint Handling Rules (CHR), a high-level language for constraint solvers, with tabled Logic Programming. The framework is easily instantiated with new application-specific constraint domains. Various high-level operations can be instantiated to control performance. In particular, we propose a novel, generalized technique for compacting answer sets.

@article{schr_warren_tchr_tplp08,
author = {Tom Schrijvers and Bart Demoen and David S. Warren},
title = {{TCHR}: a framework for tabled {CLP}},
journal = TPLP,
volume = 8,
number = 4,
month = jul,
year = 2008,
pages = {491--526},
publisHer = CUP,
doi = {10.1017/S147106840800327X},
keywords = {implementation},
abstract = { Tabled Constraint Logic Programming is a powerful execution mechanism for dealing with Constraint Logic Programming without worrying about fixpoint computation. Various applications, e.g. in the fields of program analysis and model checking, have been proposed. Unfortunately, a high-level system for developing new applications is lacking, and programmers are forced to resort to complicated ad hoc solutions. 

This papers presents TCHR, a high-level framework for tabled Constraint Logic Programming. It integrates in a light-weight manner Constraint Handling Rules (CHR), a high-level language for constraint solvers, with tabled Logic Programming. The framework is easily instantiated with new application-specific constraint domains. Various high-level operations can be instantiated to control performance. In particular, we propose a novel, generalized technique for compacting answer sets. },

}

Martin Sulzmann and Peter J. Stuckey. HM(X) Type Inference is CLP(X) Solving. Journal of Functional Programming, 18(2):251-283, 2008. [doi:10.1017/S0956796807006569] Keyword(s): type systems. Abstract:

The HM(X) system is a generalization of the Hindley/Milner system parameterized in the constraint domain X. Type inference is performed by generating constraints out of the program text, which are then solved by the domain-specific constraint solver X. The solver has to be invoked at the latest when type inference reaches a let node so that we can build a polymorphic type. A typical example of such an inference approach is Milner's algorithm W. We formalize an inference approach where the HM(X) type inference problem is first mapped to a CLP(X) program. The actual type inference is achieved by executing the CLP(X) program. Such an inference approach supports the uniform construction of type inference algorithms and has important practical consequences when it comes to reporting type errors. The CLP(X) style inference system, where X is defined by Constraint Handling Rules, is implemented as part of the Chameleon system.

@article{sulzm_stuckey_hmx_is_clpx_jfp08,
author = {Martin Sulzmann and Peter J. Stuckey},
title = {{HM(X)} Type Inference is {CLP(X)} Solving},
keywords = {type systems},
journal = {Journal of Functional Programming},
volume = 18,
number = 2,
pages = {251--283},
publisher = CUP,
year = 2008,
abstract = { The HM(X) system is a generalization of the Hindley/Milner system parameterized in the constraint domain X. Type inference is performed by generating constraints out of the program text, which are then solved by the domain-specific constraint solver X. The solver has to be invoked at the latest when type inference reaches a let node so that we can build a polymorphic type. A typical example of such an inference approach is Milner's algorithm W. We formalize an inference approach where the HM(X) type inference problem is first mapped to a CLP(X) program. The actual type inference is achieved by executing the CLP(X) program. Such an inference approach supports the uniform construction of type inference algorithms and has important practical consequences when it comes to reporting type errors. The CLP(X) style inference system, where X is defined by Constraint Handling Rules, is implemented as part of the Chameleon system. },
doi = {10.1017/S0956796807006569},

}

Hongwei Zhu, Stuart E. Madnick, and Michael D. Siegel. Enabling global price comparison through semantic integration of web data. IJEB, 6(4):319-341, 2008.

@article{zhu_madnick_siegel_IJEB08,
author = {Hongwei Zhu and Stuart E. Madnick and Michael D. Siegel},
title = {Enabling global price comparison through semantic integration of web data},
journal = {IJEB},
volume = {6},
number = {4},
pages = {319-341},
year = {2008} 
}

Henning Christiansen. Implementing Probabilistic Abductive Logic Programming with Constraint Handling Rules. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence, pages 85-118. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_5] Keyword(s): abduction, probabilistic CHR.
```
@incollection{christiansen_prob_abd_lp_lnai08,
title = {Implementing Probabilistic Abductive Logic Programming with {C}onstraint {H}andling {R}ules},
author = {Henning Christiansen},
keywords = {abduction, probabilistic CHR},
crossref = {lnai08},
year = 2008,
pages = {85--118},
doi = {10.1007/978-3-540-92243-8_5},

}
```

Leslie De Koninck, Tom Schrijvers, and Bart Demoen. A Flexible Search Framework for CHR. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence, pages 16-47. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_2] Keyword(s): disjunction, search.
```
@incollection{dekoninck_et_al_flexible_search_lnai08,
title = {A Flexible Search Framework for {CHR}},
author = {De Koninck, Leslie and Tom Schrijvers and Bart Demoen},
crossref = {lnai08},
keywords = {disjunction, search},
year = 2008,
pages = {16--47},
doi = {10.1007/978-3-540-92243-8_2},

}
```

Thom Frühwirth. Welcome to Constraint Handling Rules. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence, pages 1-15. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_1] Keyword(s): tutorial.
```
@incollection{fru_welcome_lnai08,
title = {Welcome to {C}onstraint {H}andling {R}ules},
author = {Thom Fr{\"u}hwirth},
crossref = {lnai08},
year = 2008,
pages = {1--15},
keywords = {tutorial},
doi = {10.1007/978-3-540-92243-8_1},

}
```

Maurizio Gabbrielli, Maria Chiara Meo, and Paolo Tacchella. A Compositional Semantics for CHR with Propagation Rules. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence, pages 119-160. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_6] Keyword(s): semantics.
```
@incollection{gabbrielli_meo_tacchella_comp_sem_lnai08,
title = {A Compositional Semantics for {CHR} with Propagation Rules},
author = {Maurizio Gabbrielli and Meo, Maria Chiara and Paolo Tacchella},
keywords = {semantics},
crossref = {lnai08},
year = 2008,
pages = {119--160},
doi = {10.1007/978-3-540-92243-8_6},

}
```

Jon Sneyers, Tom Schrijvers, and Bart Demoen. Guard Reasoning in the Refined Operational Semantics of CHR. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence, pages 213-244. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_8] Keyword(s): implementation, optimizing compilation.
```
@incollection{sneyers_et_al_guard_reasoning_lnai08,
title = {Guard Reasoning in the Refined Operational Semantics of {CHR}},
author = {Jon Sneyers and Tom Schrijvers and Bart Demoen},
keywords = {implementation, optimizing compilation},
crossref = {lnai08},
year = 2008,
pages = {213--244},
doi = {10.1007/978-3-540-92243-8_8},

}
```

Ingi Sobhi, Slim Abdennadher, and Hariolf Betz. Constructing Rule-Based Solvers for Intentionally-Defined Constraints. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence, pages 70-84. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_4] Keyword(s): program generation.
```
@incollection{sobhi_abd_betz_intentionally_def_constraints_lnai08,
title = {Constructing Rule-Based Solvers for Intentionally-Defined Constraints},
author = {Ingi Sobhi and Slim Abdennadher and Hariolf Betz},
keywords = {program generation},
crossref = {lnai08},
year = 2008,
pages = {70--84},
doi = {10.1007/978-3-540-92243-8_4},

}
```

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, volume 5388 of Lecture Notes in Artificial Intelligence, pages 161-212. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_7] Keyword(s): implementation, Java. Abstract:

In this paper, we address the different conceptual and technical difficulties encountered when embedding CHR into an imperative host language. We argue that a tight, natural integration leads to a powerful programming language extension, intuitive to both CHR and imperative programmers. We show how to compile CHR to highly optimized imperative code. To this end, we first review the well-established CHR compilation scheme, and survey the large body of possible optimizations. We then show that this scheme, when used for compilation to imperative target languages, leads to stack overflows. We therefore introduce new optimizations that considerably improve the performance of recursive CHR programs. Rules written using tail calls are even guaranteed to run in constant space. We implemented systems for both Java and C, following the language design principles and compilation scheme presented in this paper, and show that our implementations outperform other state-of-the-art CHR compilers by several orders of magnitude.

@incollection{vanweert_wuille_et_al_chr_imperative_lnai08,
title = {{CHR} for Imperative Host Languages},
author = {Van Weert, Peter and Wuille, Pieter and Schrijvers, Tom and Demoen, Bart},
crossref = {lnai08},
year = 2008,
keywords = {implementation, Java},
abstract = { In this paper, we address the different conceptual and technical difficulties encountered when embedding CHR into an imperative host language. We argue that a tight, natural integration leads to a powerful programming language extension, intuitive to both CHR and imperative programmers. We show how to compile CHR to highly optimized imperative code. To this end, we first review the well-established CHR compilation scheme, and survey the large body of possible optimizations. We then show that this scheme, when used for compilation to imperative target languages, leads to stack overflows. We therefore introduce new optimizations that considerably improve the performance of recursive CHR programs. Rules written using tail calls are even guaranteed to run in constant space. We implemented systems for both Java and C, following the language design principles and compilation scheme presented in this paper, and show that our implementations outperform other state-of-the-art CHR compilers by several orders of magnitude. },
pages = {161--212},
doi = {10.1007/978-3-540-92243-8_7},
url = {https://lirias.kuleuven.be/handle/123456789/197033},

}

Armin Wolf, Jacques Robin, and Jairson Vitorino. Adaptive CHR meets CHR^∨: An Extended Refined Operational Semantics for CHR^∨ Based on Justifications. In Tom Schrijvers and Thom Frühwirth, editors, Constraint Handling Rules — Current Research Topics, volume 5388 of Lecture Notes in Artificial Intelligence, pages 48-69. Springer-Verlag, December 2008. [WWW] [doi:10.1007/978-3-540-92243-8_3] Keyword(s): disjunction, search, semantics.
```
@incollection{wolf_robin_vitorino_chrv_semantics_lnai08,
title = {Adaptive {CHR} meets {CHR$^\vee$}: An Extended Refined Operational Semantics for {CHR$^\vee$} Based on Justifications},
author = {Armin Wolf and Jacques Robin and Jairson Vitorino},
keywords = {disjunction, search, semantics},
crossref = {lnai08},
year = 2008,
pages = {48--69},
doi = {10.1007/978-3-540-92243-8_3},

}
```

Conference articles

Slim Abdennadher and Shehab Fawzy. JCHRIDE: An Integrated Development Environment for JCHR. In Sibylle Schwarz, editor, WLP '08: Proc. 22nd Workshop on (Constraint) Logic Programming, Dresden, Germany, pages 1-6, September 2008. University Halle-Wittenberg, Institute of Computer Science, Technical report 2008/08. Keyword(s): Java. Abstract:

The rule-based programming language Constraint Handling Rules (CHR) has been introduced to ease the development and implementation of constraint solvers. Currently, several CHR libraries exist in languages such as Prolog, Haskell and Java. The K.U.Leuven JCHR system is a high-performance integration of Constraint Handling Rules (CHR) and Java. JCHR is currently by far the most efficient implementation of CHR in Java. Its performance is competitive with state-of-the-art CHR systems in e.g.\ HAL and Prolog. To ease the duty of a CHR programmer, we introduce in this paper an integrated development environment (IDE) for the K.U.Leuven JCHR. The IDE is implemented as a plug-in in Eclipse.

@inproceedings{abd_fawzy_jchride_wlp08,
author = {Slim Abdennadher and Shehab Fawzy},
title = {{JCHRIDE}: An {I}ntegrated {D}evelopment {E}nvironment for {JCHR}},
booktitle = {WLP '08: Proc.\ 22nd Workshop on (Constraint) Logic Programming},
pages = {1--6},
address = {Dresden, Germany},
year = 2008,
month = sep,
editor = {Sibylle Schwarz},
publisher = {University Halle-Wittenberg, Institute of Computer Science, Technical report 2008/08},
keywords = {Java},
abstract = { The rule-based programming language Constraint Handling Rules (CHR) has been introduced to ease the development and implementation of constraint solvers. Currently, several CHR libraries exist in languages such as Prolog, Haskell and Java. The K.U.Leuven JCHR system is a high-performance integration of Constraint Handling Rules (CHR) and Java. JCHR is currently by far the most efficient implementation of CHR in Java. Its performance is competitive with state-of-the-art CHR systems in e.g.\ HAL and Prolog. To ease the duty of a CHR programmer, we introduce in this paper an integrated development environment (IDE) for the K.U.Leuven JCHR. The IDE is implemented as a plug-in in Eclipse. },

}

Slim Abdennadher and Ingi Sobhi. Generation of Rule-based Constraint Solvers: Combined Approach. In A. King, editor, LOPSTR '07: 17th Intl. Symp. Logic-Based Program Synthesis and Transformation, Revised Selected Papers, volume 4915 of Lecture Notes in Computer Science, 2008. Keyword(s): program generation.
```
@inproceedings{abd_sobhi_generation_combined_lopstr07,
author = {Slim Abdennadher and Ingi Sobhi},
title = {Generation of Rule-based Constraint Solvers: Combined Approach},
keywords = {program generation},
crossref = {plopstr07} 
}
```

Marcos Aurélio, François Fages, and Jacques Robin. Default Reasoning in CHR^∨. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 111-126, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, disjunction, CHR 2008, CHR 2008. Abstract:

CHR^∨ has emerged as a versatile knowledge representation language, usable for an unparalleled variety of automated reasoning tasks: constraint solving, optimization, classification, subsumption, classical deduction, abduction, truth-maintenance, belief revision, belief update and planning. In this paper, we add default reasoning to this list, by showing how to represent default logic theories in CHR^∨. We then discuss how to leverage this representation together with the well-know correspondence between default logic and Negation As Failure (NAF) in logic programming, to propose an extension CHR$^{\vee,naf}$ of CHR^∨ allowing NAF in the rule heads.

@inproceedings{aurelio_fages_robin_defaultreasoning_chr08,
author = {Marcos Aur{\'e}lio and Fran{\c c}ois Fages and Jacques Robin},
title = {Default Reasoning in {CHR}$^\vee$},
pages = {111--126},
crossref = {pchr08},
abstract = { CHR$^\vee$ has emerged as a versatile knowledge representation language, usable for an unparalleled variety of automated reasoning tasks: constraint solving, optimization, classification, subsumption, classical deduction, abduction, truth-maintenance, belief revision, belief update and planning. In this paper, we add default reasoning to this list, by showing how to represent default logic theories in CHR$^\vee$. We then discuss how to leverage this representation together with the well-know correspondence between default logic and Negation As Failure (NAF) in logic programming, to propose an extension CHR$^{\vee,naf}$ of CHR$^\vee$ allowing NAF in the rule heads. },
keywords = {CHR 2008, disjunction},
pdf = PAPERSHOME # {chr2008.pdf#page=119},

}

Henning Christiansen. Prioritized Abduction with CHR. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 159-173, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, abduction, priorities, probabilistic CHR, CHR 2008, CHR 2008. Abstract:

A class of Prioritized Abductive Logic Programs (PrioALPs) is introduced and an implementation is developed in CHR for solving abductive problems, providing minimal explanations with best-first search. Priorities may represent probabilities or a cost function to be optimized. Compared with other weighted and probabilistic versions of abductive logic programming, the approach is characterized by higher generality and a flexible and adaptable architecture which incorporates integrity constraints and interaction with external constraint solvers. A PrioALP is translated in a systematic way into a CHR program which serves as a query interpreter, and the resulting CHR code describes in a highly concise way, the strategies applied in the search for explanations.

@inproceedings{christiansen_prioritizedabduction_chr08,
author = {Henning Christiansen},
title = {Prioritized Abduction with {CHR}},
pages = {159--173},
crossref = {pchr08},
abstract = { A class of Prioritized Abductive Logic Programs (PrioALPs) is introduced and an implementation is developed in CHR for solving abductive problems, providing minimal explanations with best-first search. Priorities may represent probabilities or a cost function to be optimized. Compared with other weighted and probabilistic versions of abductive logic programming, the approach is characterized by higher generality and a flexible and adaptable architecture which incorporates integrity constraints and interaction with external constraint solvers. A PrioALP is translated in a systematic way into a CHR program which serves as a query interpreter, and the resulting CHR code describes in a highly concise way, the strategies applied in the search for explanations. },
keywords = {CHR 2008, abduction, priorities, probabilistic CHR},
pdf = PAPERSHOME # {chr2008.pdf#page=167},

}

Leslie De Koninck, Peter J. Stuckey, and Gregory J. Duck. Optimizing compilation of CHR with rule priorities. In J. Garrigue and M. Hermenegildo, editors, Proc. 9th Intl. Symp. Functional and Logic Programming, volume 4989 of Lecture Notes in Computer Science, pages 32-47, April 2008. Springer-Verlag. Keyword(s): priorities, optimizing compilation.

@inproceedings{dekoninck_stuck_duck_compiling-chrrp_flops08,
author = {De Koninck, Leslie and Stuckey, Peter J. and Duck, Gregory J.},
title = {Optimizing compilation of {CHR} with rule priorities},
booktitle = {Proc.\ 9th Intl.\ Symp.\ Functional and Logic Programming},
month = apr,
year = 2008,
location = {Ise, Japan},
city = {Ise, Japan},
pages = {32--47},
editor = {J. Garrigue and M. Hermenegildo},
series = LNCS,
volume = {4989},
keywords = {priorities, optimizing compilation},
publisher = SV 
}

Gregory J. Duck, Leslie De Koninck, and Peter J. Stuckey. Cadmium: An Implementation of ACD Term Rewriting. In M. Garcìa de la Banda and E. Pontelli, editors, ICLP '08: Proc. 24rd Intl. Conf. Logic Programming, volume 5366 of Lecture Notes in Computer Science, pages 531-545, December 2008. Springer-Verlag. [doi:10.1007/978-3-540-89982-2] Keyword(s): implementation.
```
@inproceedings{duck_cadmium_iclp08,
title = {Cadmium: An Implementation of {ACD} Term Rewriting},
author = {Gregory J. Duck and Leslie De Koninck and Peter J. Stuckey},
keywords = {implementation},
crossref = {piclp08},
pages = {531--545},

}
```

François Fages, Cleyton Mário de Oliveira Rodrigues, and Thierry Martinez. Modular CHR with ask and tell. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 95-110, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, CHR 2008, CHR 2008. Abstract:

In this paper, we introduce a modular version of the Constraint Handling Rules language CHR, called CHRat for modular CHR with ask and tell. Any constraint defined in a CHRat component can be reused both in rules and guards in another CHRat component to define new constraint solvers. Unlike previous work on modular CHR, our approach is completely general as it does not rely on an automatic derivation of conditions for checking entailment in guards, but on a programming discipline for defining both satisfiability (tell) and entailment (ask) checks by CHRat rules for each constraint. We define the operational and declarative semantics of CHRat, provide a transformation of CHRat components to flat CHR programs, and prove the preservation of the semantics. We then provide examples of the modularization of classical CHR constraint solvers and of the definition of complex constraint solvers in a modular fashion.

@inproceedings{fages_et_al_modularchr_chr08,
author = {Fran{\c c}ois Fages and M{\'a}rio de Oliveira Rodrigues, Cleyton and Thierry Martinez},
title = {Modular {CHR} with \emph{ask} and \emph{tell}},
pages = {95--110},
crossref = {pchr08},
abstract = { In this paper, we introduce a modular version of the Constraint Handling Rules language CHR, called CHRat for modular CHR with \emph{ask} and \emph{tell}. Any constraint defined in a CHRat component can be reused both in rules and guards in another CHRat component to define new constraint solvers. Unlike previous work on modular CHR, our approach is completely general as it does not rely on an automatic derivation of conditions for checking entailment in guards, but on a programming discipline for defining both satisfiability (\emph{tell}) and entailment (\emph{ask}) checks by CHRat rules for each constraint. We define the operational and declarative semantics of CHRat, provide a transformation of CHRat components to flat CHR programs, and prove the preservation of the semantics. We then provide examples of the modularization of classical CHR constraint solvers and of the definition of complex constraint solvers in a modular fashion. },
keywords = {CHR 2008},
pdf = PAPERSHOME # {chr2008.pdf#page=103},

}

Thom Frühwirth. Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR. In Recent Advances in Constraints — CSCLP '07: 12th ERCIM Intl. Workshop on Constraint Solving and Constraint Logic Programming, Revised Selected Papers, pages 91-118, November 2008. [doi:10.1007/978-3-540-89812-2_7] Keyword(s): algorithms. Abstract:

The union-find algorithm can be seen as solving simple equations between variables or constants. With a few lines of code change, we generalise its implementation in CHR from equality to arbitrary binary relations. By choosing the appropriate relations, we can derive fast incremental algorithms for solving certain propositional logic (SAT) problems and polynomial equations in two variables. In general, we prove that when the relations are bijective functions, our generalisation yields a correct algorithm. We also show that bijectivity is a necessary condition for correctness if the relations include the identity function. The rules of our generic algorithm have additional properties that make them suitable for incorporation into constraint solvers: from classical union-find, they inherit a compact solved form and quasi-linear time and space complexity. By nature of CHR, they are anytime and online algorithms. They solve and simplify the constraints in the problem, and can test them for entailment, even when the constraints arrive incrementally.

@inproceedings{fru_general_union_find_csclp07,
author = {Thom Fr{\"u}hwirth},
title = {Quasi-Linear-Time Algorithms by Generalisation of Union-Find in {CHR}},
year = 2008,
month = nov,
location = {Rocquencourt, France},
city = {Rocquencourt, France},
booktitle = {Recent Advances in Constraints --- CSCLP '07: 12th ERCIM Intl. Workshop on Constraint Solving and Constraint Logic Programming, Revised Selected Papers},
pages = {91--118},
keywords = {algorithms},
doi = {10.1007/978-3-540-89812-2_7},
abstract = { The union-find algorithm can be seen as solving simple equations between variables or constants. With a few lines of code change, we generalise its implementation in CHR from equality to arbitrary binary relations. By choosing the appropriate relations, we can derive fast incremental algorithms for solving certain propositional logic (SAT) problems and polynomial equations in two variables. In general, we prove that when the relations are bijective functions, our generalisation yields a correct algorithm. We also show that bijectivity is a necessary condition for correctness if the relations include the identity function. 

The rules of our generic algorithm have additional properties that make them suitable for incorporation into constraint solvers: from classical union-find, they inherit a compact solved form and quasi-linear time and space complexity. By nature of CHR, they are anytime and online algorithms. They solve and simplify the constraints in the problem, and can test them for entailment, even when the constraints arrive incrementally. },

}

Marco Gavanelli, Marco Alberti, and Evelina Lamma. Integrating Abduction and Constraint Optimization in Constraint Handling Rules. In ECAI 2008: 18th European Conf. on Artif. Intell., pages 903-904, July 2008. IOS press. [doi:10.3233/978-1-58603-891-5-903] Keyword(s): abduction.

@inproceedings{gavanelli_alberti_lamma_abduction_optimization_ecai08,
author = {Marco Gavanelli and Marco Alberti and Evelina Lamma},
title = {Integrating Abduction and Constraint Optimization in {C}onstraint {H}andling {R}ules},
keywords = {abduction},
booktitle = {ECAI 2008: 18th European Conf.\ on Artif.\ Intell.},
year = 2008,
month = jul,
publisher = {IOS press},
pages = {903--904},
doi = {10.3233/978-1-58603-891-5-903},

}

Rémy Haemmerlé and Hariolf Betz. Verification of Constraint Handling Rules using Linear Logic Phase Semantics. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 67-78, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, linear logic, verification, CHR 2008, CHR 2008. Abstract:

Constraint Handling Rules (CHR) is a declarative concurrent programming language. Like the class of Concurrent Constraint (CC) languages, CHR features a declarative semantics based on Girard's intuitionistic linear logic. The phase semantics of linear logic has been used in the past to prove safety properties for the class of CC languages. In this paper we show that we can adapt this result to prove safety properties for CHR as well.

@inproceedings{haemerle_betz_verificationlinearlogicphase_chr08,
author = {R{\'e}my Haemmerl{\'e} and Hariolf Betz},
title = {Verification of {C}onstraint {H}andling {R}ules using Linear Logic Phase Semantics},
pages = {67--78},
crossref = {pchr08},
abstract = { Constraint Handling Rules (CHR) is a declarative concurrent programming language. Like the class of Concurrent Constraint (CC) languages, CHR features a declarative semantics based on Girard's intuitionistic linear logic. The phase semantics of linear logic has been used in the past to prove safety properties for the class of CC languages. In this paper we show that we can adapt this result to prove safety properties for CHR as well. },
keywords = {CHR 2008, linear logic, verification},
pdf = PAPERSHOME # {chr2008.pdf#page=75},

}

Edmund S.L. Lam and Martin Sulzmann. Finally, A Comparison Between Constraint Handling Rules and Join-Calculus. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 51-66, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, related formalisms, CHR 2008, CHR 2008. Abstract:

We provide a comparison between Constraint Handling Rules and Join-Calculus. Constraint Handling Rules is a concurrent constraint programming language originally designed for writing constraint solvers. Join-Calculus is a process calculus designed to provide the programmer with expressive concurrency abstraction. The semantics of both calculi is based on the Chemical Abstract Machine. Hence, we expect that both calculi share some commonalities. Surprisingly, both calculi have thus far been studied independently, yet we believe that a comparison of these two independent fields of study is long overdue. This paper establishes a first bridge between Constraint Handling Rules and Join-Calculus as a basis for future explorations. Specifically, we provide examples showing that Join-Calculus can benefit from guarded constraints and constraint propagation as found in Constraint Handling Rules. We provide a compilation scheme for such an enriched Join-Calculus by applying the constraint matching methods of the refined operational Constraint Handling Rules semantics.

@inproceedings{lam_sulz_finallyjoin_chr08,
author = {Edmund S.L. Lam and Martin Sulzmann},
title = {Finally, A Comparison Between {C}onstraint {H}andling {R}ules and Join-Calculus},
pages = {51--66},
crossref = {pchr08},
abstract = { We provide a comparison between Constraint Handling Rules and Join-Calculus. Constraint Handling Rules is a concurrent constraint programming language originally designed for writing constraint solvers. Join-Calculus is a process calculus designed to provide the programmer with expressive concurrency abstraction. The semantics of both calculi is based on the Chemical Abstract Machine. Hence, we expect that both calculi share some commonalities. Surprisingly, both calculi have thus far been studied independently, yet we believe that a comparison of these two independent fields of study is long overdue. This paper establishes a first bridge between Constraint Handling Rules and Join-Calculus as a basis for future explorations. Specifically, we provide examples showing that Join-Calculus can benefit from guarded constraints and constraint propagation as found in Constraint Handling Rules. We provide a compilation scheme for such an enriched Join-Calculus by applying the constraint matching methods of the refined operational Constraint Handling Rules semantics. },
keywords = {CHR 2008, related formalisms},
pdf = PAPERSHOME # {chr2008.pdf#page=59},

}

Paolo Pilozzi and Danny De Schreye. Termination Analysis of CHR Revisited. In M. Garcìa de la Banda and E. Pontelli, editors, ICLP '08: Proc. 24rd Intl. Conf. Logic Programming, volume 5366 of Lecture Notes in Computer Science, pages 501-515, December 2008. Springer-Verlag. [doi:10.1007/978-3-540-89982-2_43] Keyword(s): termination. Abstract:

Today, two distinct direct approaches to prove termination of CHR programs exist. The first approach, by T. Fr\"uhwirth, proves termination of CHR programs without propagation. The second, by Voets et al., deals with programs that contain propagation. It is however less powerful on programs without propagation. In this paper, we present new termination conditions that are strictly more powerful than those from previous approaches and that are also applicable to a new class of programs. Furthermore, we present a new representation for CHR states for which size-decreases between consecutive states correspond to termination. Both contributions are linked: our termination conditions correspond to the existence of a well-founded order on the new state representation, which decreases for consecutive computation states.

@inproceedings{pilozzi_deschreye_termination_revisited_iclp08,
author = {Paolo Pilozzi and De Schreye, Danny},
title = {Termination Analysis of {CHR} Revisited},
crossref = {piclp08},
pages = {501--515},
abstract = { Today, two distinct direct approaches to prove termination of CHR programs exist. The first approach, by T. Fr\"uhwirth, proves termination of CHR programs without propagation. The second, by Voets et al., deals with programs that contain propagation. It is however less powerful on programs without propagation. In this paper, we present new termination conditions that are strictly more powerful than those from previous approaches and that are also applicable to a new class of programs. Furthermore, we present a new representation for CHR states for which size-decreases between consecutive states correspond to termination. Both contributions are linked: our termination conditions correspond to the existence of a well-founded order on the new state representation, which decreases for consecutive computation states. },
keywords = {termination},
doi = {10.1007/978-3-540-89982-2_43},

}

Paolo Pilozzi and Danny De Schreye. Termination Analysis of CHR revisited. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 35-50, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, termination, CHR 2008, CHR 2008. Abstract:

Today, there exist two distinct direct approaches to prove termination of CHR programs. Both are applicable on separate classes of CHR programs. One approach, by T. Fr{\"u}hwirth, proves termination of CHR programs without propagation rules. A second approach deals with CHR programs with propagation rules. Due to its extended scope to such programs, it fails to prove termination for a class of CHR programs without propagation that are in the scope of Fr{\"u}hwirth's approach. In this paper, we introduce a termination condition for CHR which is strictly more powerful than both of these and deals with a new class of programs.

@inproceedings{pilozzi_deschreye_terminationrevisited_chr08,
author = {Pilozzi, Paolo and De Schreye, Danny},
title = {Termination Analysis of {CHR} revisited},
pages = {35--50},
crossref = {pchr08},
abstract = { Today, there exist two distinct direct approaches to prove termination of CHR programs. Both are applicable on separate classes of CHR programs. One approach, by T. Fr{\"u}hwirth, proves termination of CHR programs without propagation rules. A second approach deals with CHR programs with propagation rules. Due to its extended scope to such programs, it fails to prove termination for a class of CHR programs without propagation that are in the scope of Fr{\"u}hwirth's approach. In this paper, we introduce a termination condition for CHR which is strictly more powerful than both of these and deals with a new class of programs. },
keywords = {CHR 2008, termination},
pdf = PAPERSHOME # {chr2008.pdf#page=43},

}

Frank Raiser. Semi-automatic generation of CHR solvers from global constraint automata. In Peter J. Stuckey, editor, CP' 08: Proc. 14th Intl. Conf. Princ. Pract. Constraint Programming, volume 5202 of Lecture Notes in Computer Science, pages 588-592, September 2008. Springer-Verlag. [doi:10.1007/978-3-540-85958-1_47] Keyword(s): program generation. Abstract:

Constraint programming often involves global constraints, for which various custom filtering algorithms have been published. This work presents a semi-automatic generation of CHR solvers for the subset of global constraints defineable by specific automata. The generation is based on a constraint logic program modelling an automaton and an improved version of the Prim-Miner algorithm. The solvers only need to be generated once and achieve arc-consistency for over 40 global constraints.

@inproceedings{raiser_globalconstraintautomata_cp08,
author = {Frank Raiser},
title = {Semi-automatic generation of {CHR} solvers from global constraint automata},
booktitle = CP08l,
editor = {Peter J. Stuckey},
pages = {588--592},
series = LNCS,
volume = 5202,
publisher = SV,
location = {Sydney, Australia},
city = {Sydney, Australia},
year = 2008,
month = sep,
doi = {10.1007/978-3-540-85958-1_47},
keywords = {program generation},
abstract = { Constraint programming often involves global constraints, for which various custom filtering algorithms have been published. This work presents a semi-automatic generation of CHR solvers for the subset of global constraints defineable by specific automata. The generation is based on a constraint logic program modelling an automaton and an improved version of the Prim-Miner algorithm. The solvers only need to be generated once and achieve arc-consistency for over 40 global constraints. },

}

Frank Raiser and Thom Frühwirth. Towards Term Rewriting Systems in Constraint Handling Rules. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 19-34, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): related formalisms, CHR 2008, CHR 2008, CHR 2008. Abstract:

Term rewriting systems are a formalism in widespread use, often implemented by means of term graph rewriting. In this work we present preliminary results towards an elegant embedding of term graph rewriting in Constraint Handling Rules with rule priorities (CHR^rp). As term graph rewriting is well-known to be incomplete with respect to term rewriting, we aim for sound jungle evaluation in CHR^rp. Having such an embedding available allows to benefit from CHR's online property and parallelization potential.

@inproceedings{raiser_fru_towardstermrewriting_chr08,
author = {Frank Raiser and Thom Fr{\"u}hwirth},
title = {Towards Term Rewriting Systems in {C}onstraint {H}andling {R}ules},
pages = {19--34},
crossref = {pchr08},
abstract = { Term rewriting systems are a formalism in widespread use, often implemented by means of term graph rewriting. In this work we present preliminary results towards an elegant embedding of term graph rewriting in Constraint Handling Rules with rule priorities ($\mathrm{CHR}^\mathrm{rp}$). As term graph rewriting is well-known to be incomplete with respect to term rewriting, we aim for sound jungle evaluation in $\mathrm{CHR}^\mathrm{rp}$. Having such an embedding available allows to benefit from CHR's online property and parallelization potential. },
keywords = {related formalisms},
keywords = {CHR 2008},
pdf = PAPERSHOME # {chr2008.pdf#page=27},

}

Beata Sarna-Starosta and Tom Schrijvers. An efficient term representation for CHR indexing. In M. Carro and B. Demoen, editors, CICLOPS '08: Proc. 8th Colloquium on Implementation of Constraint and LOgic Programming Systems, pages 172-186, 2008. Keyword(s): implementation, optimizing compilation.

@inproceedings{sss_term_indexing_ciclops08,
author = {Beata Sarna-Starosta and Tom Schrijvers},
title = {An efficient term representation for {CHR} indexing},
keywords = {implementation, optimizing compilation},
booktitle = {CICLOPS '08: Proc.\ 8th Colloquium on Implementation of Constraint and LOgic Programming Systems},
editor = {M. Carro and B. Demoen},
pages = {172--186},
year = 2008,

}

Beata Sarna-Starosta and Tom Schrijvers. Transformation-based Indexing Techniques for Constraint Handling Rules. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 3-18, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): implementation, optimizing compilation, CHR 2008, CHR 2008, CHR 2008. Abstract:

Multi-headed rules are essential for the expressiveness of Constraint Handling Rules (CHR), but incur considerable performance overhead. Current indexing techniques are often unable to address this problemâ€”they require matchings to have particular form, or offer good run-time complexity rather than good absolute figures. We introduce two lightweight program transformations, based on term flattening, which improve the effectiveness of existing CHR indexing techniques, in terms of both complexity and constant factors. We also describe a set of complementary post-processing program transformations, which considerably reduce the flattening overhead. We compare our techniques with the current state of the art in CHR compilation, and measure their efficacy in K.U.Leuven CHR and CHRd.

@inproceedings{sarnastarosta_schr_transform_indexing_chr08,
author = {Beata Sarna-Starosta and Tom Schrijvers},
title = {Transformation-based Indexing Techniques for {C}onstraint {H}andling {R}ules},
keywords = {implementation, optimizing compilation},
pages = {3--18},
crossref = {pchr08},
abstract = { Multi-headed rules are essential for the expressiveness of Constraint Handling Rules (CHR), but incur considerable performance overhead. Current indexing techniques are often unable to address this problemâ€”they require matchings to have particular form, or offer good run-time complexity rather than good absolute figures. We introduce two lightweight program transformations, based on term flattening, which improve the effectiveness of existing CHR indexing techniques, in terms of both complexity and constant factors. We also describe a set of complementary post-processing program transformations, which considerably reduce the flattening overhead. We compare our techniques with the current state of the art in CHR compilation, and measure their efficacy in K.U.Leuven CHR and CHRd. },
keywords = {CHR 2008},
pdf = PAPERSHOME # {chr2008.pdf#page=13},

}

Beata Sarna-Starosta, David Zook, Emir Pasalic, and Molham Aref. Relating Constraint Handling Rules to Datalog. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 127-142, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, related formalisms, CHR 2008, CHR 2008. Abstract:

Datalog^LB is an extension of Datalog supporting global stratification of negation and functional dependencies, designed for use in industrial-scale decision automation applications. Constraint Handling Rules (CHR) is a declarative rule-based programming language, particularly suitable for specifying custom constraint solvers at a high level. Our goal is to enhance Datalog^LB with CHR-like capabilities in order to improve its expressive power and open it to specification of general-purpose constraint solvers for industrial applications. In this paper we relate the two formalisms and define a translation of a significant class of CHR programs into Datalog^LB. It turns out that the translation enables reasoning about the properties of CHR programs at a high level of Datalog logic.

@inproceedings{sarnastarosta_pasalic_datalog_chr08,
author = {Beata Sarna-Starosta and David Zook and Emir Pasalic and Molham Aref},
title = {Relating {C}onstraint {H}andling {R}ules to Datalog},
pages = {127--142},
crossref = {pchr08},
abstract = { Datalog$^	extsc{LB}$ is an extension of Datalog supporting global stratification of negation and functional dependencies, designed for use in industrial-scale decision automation applications. Constraint Handling Rules (CHR) is a declarative rule-based programming language, particularly suitable for specifying custom constraint solvers at a high level. Our goal is to enhance Datalog$^	extsc{LB}$ with CHR-like capabilities in order to improve its expressive power and open it to specification of general-purpose constraint solvers for industrial applications. In this paper we relate the two formalisms and define a translation of a significant class of CHR programs into Datalog$^	extsc{LB}$. It turns out that the translation enables reasoning about the properties of CHR programs at a high level of Datalog logic. },
keywords = {CHR 2008, related formalisms},
pdf = PAPERSHOME # {chr2008.pdf#page=135},

}

Anders Schack-Nielsen and Carsten Schürmann. The CHR-Celf Connection. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 1-2, 2008. RISC Report Series 08-10, University of Linz, Austria. Note: Invited Talk. [PDF] Keyword(s): CHR 2008, related formalisms, CHR 2008, CHR 2008. Abstract:

Celf is a meta-language for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, process algebras, and logics. It is based on the concurrent logical framework CLF. The Constraint Handling Rules (CHR) language is a major specification and implementation language for constraint-based algorithms. In this invited talk, we give a tutorial-style introduction to Celf for the CHR programmer where we highlight some of Celf's features including the support of higher-order encodings, first-class execution traces, and a logically inspired proof search semantics. Furthermore we show where the semantics of the two languages coincide.

@inproceedings{sch_sch_chrcelf_chr08,
author = {Anders Schack-Nielsen and Carsten Sch{\"u}rmann},
title = {The {CHR-Celf} Connection},
pages = {1--2},
crossref = {pchr08},
note = {Invited Talk},
abstract = { Celf is a meta-language for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, process algebras, and logics. It is based on the concurrent logical framework CLF. The Constraint Handling Rules (CHR) language is a major specification and implementation language for constraint-based algorithms. In this invited talk, we give a tutorial-style introduction to Celf for the CHR programmer where we highlight some of Celf's features including the support of higher-order encodings, first-class execution traces, and a logically inspired proof search semantics. Furthermore we show where the semantics of the two languages coincide. },
keywords = {CHR 2008},
keywords = {related formalisms},
pdf = PAPERSHOME # {chr2008.pdf#page=9},

}

Tom Schrijvers. Constraint Handling Rules — A Tutorial for (Prolog) Programmers. In M. Garcìa de la Banda and E. Pontelli, editors, ICLP '08: Proc. 24rd Intl. Conf. Logic Programming, volume 5366 of Lecture Notes in Computer Science, pages 9-10, December 2008. Springer-Verlag. [doi:10.1007/978-3-540-89982-2_3] Keyword(s): tutorial.
```
@inproceedings{schr_tutorial_iclp08,
author = {Tom Schrijvers},
title = {{C}onstraint {H}andling {R}ules --- A Tutorial for ({P}rolog) Programmers},
keywords = {tutorial},
crossref = {piclp08},
pages = {9--10},
doi = {10.1007/978-3-540-89982-2_3},

}
```

Tom Schrijvers and Martin Sulzmann. Restoring confluence for functional dependencies. In Draft Proc. 9th Symp. Trends in Funct. Programming, Nijmegen, pages 22-36, May 2008. Radbound University. Keyword(s): type systems, confluence. Abstract:

Functional dependencies provide for a relational specification of user-programmable type improvement connected to type class instances. On the other hand, the more recent type families (also known as type functions) equip the programmer with a functional specification for user-programmable type improvement decoupled from type class instances. Functional dependencies are supported by both GHC and Hugs, while the most recent version of GHC also supports type functions. There is an enthusiastic and lively debate which feature shall make it into the next Haskell standard, Haskell-Prime. Currently, further progress in the standardization appears to be stalled on this issue. In this paper, we attempt to rekindle the debate with new insights in type inference issues behind functional dependencies (FDs) and type functions (TFs), without taking sides.

@inproceedings{schr_sulz_restoring_confl_fd_tfp08,
author = {Tom Schrijvers and Martin Sulzmann},
title = {Restoring confluence for functional dependencies},
booktitle = {Draft Proc.\ 9th Symp.\ Trends in Funct.\ Programming},
pages = {22--36},
month = may,
year = 2008,
address = {Nijmegen},
publisher = {Radbound University},
abstract = { Functional dependencies provide for a relational specification of user-programmable type improvement connected to type class instances. On the other hand, the more recent type families (also known as type functions) equip the programmer with a functional specification for user-programmable type improvement decoupled from type class instances. Functional dependencies are supported by both GHC and Hugs, while the most recent version of GHC also supports type functions. There is an enthusiastic and lively debate which feature shall make it into the next Haskell standard, Haskell-Prime. Currently, further progress in the standardization appears to be stalled on this issue. 

In this paper, we attempt to rekindle the debate with new insights in type inference issues behind functional dependencies (FDs) and type functions (TFs), without taking sides. },
keywords = {type systems, confluence},

}

Tom Schrijvers and Martin Sulzmann. Transactions in Constraint Handling Rules. In M. Garcìa de la Banda and E. Pontelli, editors, ICLP '08: Proc. 24rd Intl. Conf. Logic Programming, volume 5366 of Lecture Notes in Computer Science, pages 516-530, December 2008. Springer-Verlag. [doi:10.1007/978-3-540-89982-2_44] Keyword(s): parallelism. Abstract:

CHR is a highly concurrent language, and yet it is by no means a trivial task to write correct concurrent CHR programs. We propose a new semantics for CHR, which allows specifying and reasoning about transactions. Transactions alleviate the complexity of writing concurrent programs by offering entire derivations to run atomically and in isolation. We derive several program transformations based on our semantics that transform particular classes of transitional CHR programs to non-transactional ones. These transformations are useful because they obviate a general purpose transaction manager, and may lift unnecessary sequentialization present in the transactional semantics.

@inproceedings{schr_sulz_transactions_iclp08,
author = {Tom Schrijvers and Martin Sulzmann},
title = {Transactions in {C}onstraint {H}andling {R}ules},
crossref = {piclp08},
pages = {516--530},
abstract = { CHR is a highly concurrent language, and yet it is by no means a trivial task to write correct concurrent CHR programs. We propose a new semantics for CHR, which allows specifying and reasoning about transactions. Transactions alleviate the complexity of writing concurrent programs by offering entire derivations to run atomically and in isolation. 

We derive several program transformations based on our semantics that transform particular classes of transitional CHR programs to non-transactional ones. These transformations are useful because they obviate a general purpose transaction manager, and may lift unnecessary sequentialization present in the transactional semantics. },
keywords = {parallelism},
doi = {10.1007/978-3-540-89982-2_44},

}

Jon Sneyers. Turing-complete Subclasses of CHR. In M. Garcìa de la Banda and E. Pontelli, editors, ICLP '08: Proc. 24rd Intl. Conf. Logic Programming, volume 5366 of Lecture Notes in Computer Science, pages 759-763, December 2008. Springer-Verlag. [doi:10.1007/978-3-540-89982-2_72] Keyword(s): computability.
```
@inproceedings{sneyers_subclass_iclp08,
author = {Jon Sneyers},
title = {{T}uring-complete Subclasses of {CHR}},
keywords = {computability},
crossref = {piclp08},
pages = {759--763},
doi = {10.1007/978-3-540-89982-2_72},

}
```

Jon Sneyers and Thom Frühwirth. Generalized CHR Machines. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 143-158, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, complexity, CHR 2008, CHR 2008. Abstract:

Constraint Handling Rules (CHR) is a high-level rule-based programming language. In earlier work, a model of computation based on the operational semantics of CHR called the CHR machine was introduced. The CHR machine was used to prove a complexity-wise completeness result for the CHR language and its implementations. In this paper, we investigate three generalizations of CHR machines: CHR machines with an instantiated operational semantics, non-deterministic CHR machines, and self-modifying CHR machines.

@inproceedings{sneyers_fru_generalizedmachines_chr08,
author = {Jon Sneyers and Thom Fr{\"u}hwirth},
title = {Generalized {CHR} Machines},
pages = {143--158},
crossref = {pchr08},
abstract = { Constraint Handling Rules (CHR) is a high-level rule-based programming language. In earlier work, a model of computation based on the operational semantics of CHR called the CHR machine was introduced. The CHR machine was used to prove a complexity-wise completeness result for the CHR language and its implementations. In this paper, we investigate three generalizations of CHR machines: CHR machines with an instantiated operational semantics, non-deterministic CHR machines, and self-modifying CHR machines. },
keywords = {CHR 2008, complexity},
pdf = PAPERSHOME # {chr2008.pdf#page=151},

}

Martin Sulzmann and Duc Hiep Chu. A Rule-Based Specification of Software Transactional Memory. In M. Hanus, editor, LOPSTR '08: 18th Intl. Symp. Logic-Based Program Synthesis and Transformation, Pre-Proceedings, 2008. [WWW] [PDF] Keyword(s): parallelism. Abstract:

Software Transactional Memory (STM) has the promise to avoid the common pitfalls of locks when writing thread-based concurrent programs. Many papers on the subject deal with low-level implementation details to support the efficient and concurrent execution of multiple transactions.We give a rule-based specification of Software Transactional Memory in terms of Constraint Handling Rules (CHR) which naturally supports the concurrent execution of transactions. Such a high-level description of STM in terms of CHR has the advantage that we can easier understand the workings of STM and we can better analyze and verify STM. We verify correctness of a particular CHR-based STM implementation.

@inproceedings{sulzm_chu_lopstr08,
author = {Martin Sulzmann and Duc Hiep Chu},
title = {A Rule-Based Specification of {S}oftware {T}ransactional {M}emory},
crossref = {plopstr08pre},
keywords = {parallelism},
abstract = { Software Transactional Memory (STM) has the promise to avoid the common pitfalls of locks when writing thread-based concurrent programs. Many papers on the subject deal with low-level implementation details to support the efficient and concurrent execution of multiple transactions.We give a rule-based specification of Software Transactional Memory in terms of Constraint Handling Rules (CHR) which naturally supports the concurrent execution of transactions. Such a high-level description of STM in terms of CHR has the advantage that we can easier understand the workings of STM and we can better analyze and verify STM. We verify correctness of a particular CHR-based STM implementation. },

}

Martin Sulzmann and Edmund S.L. Lam. Parallel execution of multi-set constraint rewrite rules. In S. Antoy, editor, PPDP '08: Proc. 10th Intl. Conf. Princ. Pract. Declarative Programming, pages 20-31, July 2008. ACM Press. [doi:10.1145/1389449.1389453] Keyword(s): parallelism.

@inproceedings{sulz_lam_parallelexecution_ppdp08,
author = {Martin Sulzmann and Edmund S.L. Lam},
title = {Parallel execution of multi-set constraint rewrite rules},
booktitle = PPDP08l,
year = 2008,
month = jul,
editor = {S. Antoy},
location = {Valencia, Spain},
city = {Valencia, Spain},
pages = {20--31},
publisher = ACM,
keywords = {parallelism},
doi = {10.1145/1389449.1389453},

}

Martin Sulzmann, Edmund S.L. Lam, and Peter Van Weert. Actors with Multi-Headed Message Receive Patterns. In D. Lea and G. Zavattaro, editors, COORDINATION '08: Proc. 10th Intl. Conf. Coordination Models and Languages, number 5052 of Lecture Notes in Computer Science, pages 315-330, May 2008. Springer-Verlag. [doi:10.1007/978-3-540-68265-3_20] Keyword(s): parallelism. Abstract:

The actor model provides high-level concurrency abstractions to coordinate simultaneous computations by message passing. Languages implementing the actor model such as Erlang commonly only support single-headed pattern matching over received messages. We propose and design an extension of Erlang style actors with receive clauses containing multi-headed message patterns. Patterns may be non-linear and constrained by guards. We provide a number of examples to show the usefulness of the extension. We also explore the design space for multi-headed message matching semantics, for example first-match and rule priority-match semantics. The various semantics are inspired by the multi-set constraint matching semantics found in Constraint Handling Rules. This provides us with a formal model to study actors with multi-headed message receive patterns. The system can be implemented efficiently and we have built a prototype as a library-extension to Haskell.

@inproceedings{sulz_lam_vanweert_actors_coordination08,
author = {Martin Sulzmann and Edmund S.L. Lam and Van Weert, Peter},
title={Actors with Multi-Headed Message Receive Patterns},
booktitle = {COORDINATION '08: Proc.\ 10th Intl.\ Conf.\ Coordination Models and Languages},
year = 2008,
month = may,
editor = {D. Lea and G. Zavattaro},
location = {Oslo, Norway},
city = {Oslo, Norway},
pages = {315--330},
series = LNCS,
number = 5052,
publisher = SV,
keywords = {parallelism},
abstract = { The actor model provides high-level concurrency abstractions to coordinate simultaneous computations by message passing. Languages implementing the actor model such as Erlang commonly only support single-headed pattern matching over received messages. We propose and design an extension of Erlang style actors with receive clauses containing multi-headed message patterns. Patterns may be non-linear and constrained by guards. We provide a number of examples to show the usefulness of the extension. We also explore the design space for multi-headed message matching semantics, for example first-match and rule priority-match semantics. The various semantics are inspired by the multi-set constraint matching semantics found in Constraint Handling Rules. This provides us with a formal model to study actors with multi-headed message receive patterns. The system can be implemented efficiently and we have built a prototype as a library-extension to Haskell. },
doi = {10.1007/978-3-540-68265-3_20},

}

Peter Van Weert. A Tale of Histories. In T. Schrijvers, F. Raiser, and T. Frühwirth, editors, CHR '08: Proc. 5th Workshop on Constraint Handling Rules, pages 79-94, 2008. RISC Report Series 08-10, University of Linz, Austria. [PDF] Keyword(s): CHR 2008, implementation, optimizing compilation, CHR 2008, CHR 2008. Abstract:

Constraint Handling Rules (CHR) is an elegant, high-level programming language based on multi-headed, forward chaining rules. A distinguishing feature of CHR are propagation rules. To avoid trivial non-termination, CHR implementations ensure a CHR rule is applied at most once with the same combination of constraints by maintaining a so-called propagation history. The performance impact of this history is often significant. We introduce two optimizations to reduce or even eliminate this overhead, and evaluate their implementation in two state-of-the-art CHR systems.

@inproceedings{vanweert_histories_chr08,
author = {Van Weert, Peter},
title = {A Tale of Histories},
pages = {79--94},
crossref = {pchr08},
abstract = { Constraint Handling Rules (CHR) is an elegant, high-level programming language based on multi-headed, forward chaining rules. A distinguishing feature of CHR are propagation rules. To avoid trivial non-termination, CHR implementations ensure a CHR rule is applied at most once with the same combination of constraints by maintaining a so-called propagation history. The performance impact of this history is often significant. We introduce two optimizations to reduce or even eliminate this overhead, and evaluate their implementation in two state-of-the-art CHR systems. },
keywords = {CHR 2008, implementation, optimizing compilation},
pdf = PAPERSHOME # {chr2008.pdf#page=87},

}

Peter Van Weert. Optimization of CHR Propagation Rules. In M. Garcìa de la Banda and E. Pontelli, editors, ICLP '08: Proc. 24rd Intl. Conf. Logic Programming, volume 5366 of Lecture Notes in Computer Science, pages 485-500, December 2008. Springer-Verlag. [doi:10.1007/978-3-540-89982-2_42] Keyword(s): implementation, optimizing compilation. Abstract:

Constraint Handling Rules (CHR) is an elegant, high-level programming language based on multi-headed, forward chaining rules. To ensure CHR propagation rules are applied at most once with the same combination of constraints, CHR implementations maintain a so-called propagation history. The performance impact of this history can be significant. We introduce several optimizations that, for the majority of CHR rules, eliminate this overhead. We formally prove their correctness, and evaluate their implementation in two state-of-the-art CHR systems.

@inproceedings{vanweert_histories_iclp08,
author = {Van Weert, Peter},
title = {Optimization of {CHR} Propagation Rules},
keywords = {implementation, optimizing compilation},
crossref = {piclp08},
pages = {485--500},
abstract = { Constraint Handling Rules (CHR) is an elegant, high-level programming language based on multi-headed, forward chaining rules. To ensure CHR propagation rules are applied at most once with the same combination of constraints, CHR implementations maintain a so-called propagation history. The performance impact of this history can be significant. We introduce several optimizations that, for the majority of CHR rules, eliminate this overhead. We formally prove their correctness, and evaluate their implementation in two state-of-the-art CHR systems. },
doi = {10.1007/978-3-540-89982-2_42},

}

Peter Van Weert, Jon Sneyers, and Bart Demoen. Aggregates for CHR through Program Transformation. In A. King, editor, LOPSTR '07: 17th Intl. Symp. Logic-Based Program Synthesis and Transformation, Revised Selected Papers, volume 4915 of Lecture Notes in Computer Science, pages 59-73, 2008. [doi:10.1007/978-3-540-78769-3_5] Keyword(s): extensions.
```
@inproceedings{vanweert_sney_demoen_aggregates_lopstr07,
author = {Van Weert, Peter and Jon Sneyers and Bart Demoen},
title = {Aggregates for {CHR} through Program Transformation},
keywords = {extensions},
crossref = {plopstr07},
pages = {59--73},
doi = {10.1007/978-3-540-78769-3_5},

}
```

Dean Voets, Paolo Pilozzi, and Danny De Schreye. A new approach to termination analysis of CHR. In M. Hanus, editor, LOPSTR '08: 18th Intl. Symp. Logic-Based Program Synthesis and Transformation, Pre-Proceedings, 2008. [WWW] [PDF] Keyword(s): termination. Abstract:

We present a new approach to termination analysis of Constraint Handling Rules (CHR). Unlike current approaches, our approach has no restrictions on the kind of rules in the CHR program. We propose a termination condition, that verifies conditions imposed on the dynamic process of adding constraints to the store, instead of a termination argument based on the comparison of sizes of consecutive computation states. We demonstrate the condition's applicability on a set of terminating CHR programs, using a prototype analyzer. This analyzer is the first in-language automated termination analyzer for CHR programs.

@inproceedings{voets_pilozzi_deschreye_termination_lopstr08,
author = {Voets, Dean and Pilozzi, Paolo and De Schreye, Danny},
title = {A new approach to termination analysis of {CHR}},
crossref = {plopstr08pre},
keywords = {termination},
abstract = { We present a new approach to termination analysis of Constraint Handling Rules (CHR). Unlike current approaches, our approach has no restrictions on the kind of rules in the CHR program. We propose a termination condition, that verifies conditions imposed on the dynamic process of adding constraints to the store, instead of a termination argument based on the comparison of sizes of consecutive computation states. We demonstrate the condition's applicability on a set of terminating CHR programs, using a prototype analyzer. This analyzer is the first in-language automated termination analyzer for CHR programs. },

}

Internal reports

Frank Raiser. Semi-automatic generation of CHR solvers from global constraint automata. Ulmer Informatik Berichte 2008-03, Ulm University, Germany, February 2008. [WWW] Keyword(s): program generation.

@techreport{raiser_globalconstraintautomata_techrep08,
author = {Frank Raiser},
title = {Semi-automatic generation of {CHR} solvers from global constraint automata},
keywords = {program generation},
type = {Ulmer Informatik Berichte},
number = {2008-03},
institution = {Ulm University, Germany},
month = feb,
year = 2008,
url = {http://nbn-resolving.de/urn:nbn:de:bsz:289-vts-63227},

}

Peter Van Weert. Compiling Constraint Handling Rules to Java: A Reconstruction. Technical report CW 521, K.U.Leuven, Department of Computer Science, Leuven, Belgium, August 2008. [WWW] Keyword(s): Java. Abstract:

In this report, we provide a detailed description of the compilation scheme the K.U.Leuven JCHR system uses to compile CHR to efficient Java code. We start from a relatively straightforward adaptation of the traditional CHR compilation scheme for Prolog, and gradually add all its basic optimizations. Next, we show why this compilation scheme is not suited for compilation to an imperative host language such as Java. We therefore introduce a novel compilation scheme from CHR to Java that uses explicit call stack maintenance and trampoline-style compilation to guarantee that executing recursive CHR programs no longer results in call stack overflows. The empirical evaluation of the improved compilation scheme confirms it is mostly superior to the traditional one.

@techreport{vanweert_jchr_compilation_techrep08,
author = {Van Weert, Peter},
title = {Compiling {C}onstraint {H}andling {R}ules to {J}ava: A Reconstruction},
year = 2008,
month = aug,
institution = KULCW,
address = {Leuven, Belgium},
number = {CW 521},
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW521.abs.html},
keywords = {Java},
abstract = { In this report, we provide a detailed description of the compilation scheme the K.U.Leuven JCHR system uses to compile CHR to efficient Java code. We start from a relatively straightforward adaptation of the traditional CHR compilation scheme for Prolog, and gradually add all its basic optimizations. Next, we show why this compilation scheme is not suited for compilation to an imperative host language such as Java. We therefore introduce a novel compilation scheme from CHR to Java that uses explicit call stack maintenance and trampoline-style compilation to guarantee that executing recursive CHR programs no longer results in call stack overflows. The empirical evaluation of the improved compilation scheme confirms it is mostly superior to the traditional one. } 
}

Peter Van Weert. Optimization of CHR Propagation Rules: Extended report. Technical report CW 519, K.U.Leuven, Department of Computer Science, Leuven, Belgium, August 2008. [WWW] Keyword(s): implementation, optimizing compilation. Abstract:

@techreport{vanweert_histories_techrep08,
author = {Van Weert, Peter},
title = {Optimization of {CHR} Propagation Rules: Extended report},
institution = KULCW,
address = {Leuven, Belgium},
number = {CW 519},
year = 2008,
month = aug,
keywords = {implementation, optimizing compilation},
abstract = { Constraint Handling Rules (CHR) is an elegant, high-level programming language based on multi-headed, forward chaining rules. To ensure CHR propagation rules are applied at most once with the same combination of constraints, CHR implementations maintain a so-called propagation history. The performance impact of this history can be significant. We introduce several optimizations that, for the majority of CHR rules, eliminate this overhead. We formally prove their correctness, and evaluate their implementation in two state-of-the-art CHR systems. This extended report contains complete formal proofs of all theoretical results. },
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW519.abs.html},

}

Dean Voets, Paolo Pilozzi, and Danny De Schreye. A new approach to termination analysis of CHR. Technical report CW 506, K.U.Leuven, Department of Computer Science, Leuven, Belgium, January 2008. [WWW] Keyword(s): termination. Abstract:

@techreport{voets_pilozzi_deschreye_termination_techrep08,
author = {Voets, Dean and Pilozzi, Paolo and De Schreye, Danny},
title = {A new approach to termination analysis of {CHR}},
year = 2008,
month = jan,
institution = KULCW,
address = {Leuven, Belgium},
number = {CW 506},
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW506.abs.html},
abstract = { We present a new approach to termination analysis of Constraint Handling Rules (CHR). Unlike current approaches, our approach has no restrictions on the kind of rules in the CHR program. We propose a termination condition, that verifies conditions imposed on the dynamic process of adding constraints to the store, instead of a termination argument based on the comparison of sizes of consecutive computation states. We demonstrate the condition's applicability on a set of terminating CHR programs, using a prototype analyzer. This analyzer is the first in-language automated termination analyzer for CHR programs. },
keywords = {termination},

}

Miscellaneous

Scientific Software & Systems Ltd.. Company Profile: Solving problems with proven solutions, 2008. [WWW]

@misc{sssltd_2008,
author = {{Scientific Software \& Systems Ltd.}},
title = {{Company Profile: Solving problems with proven solutions}},
url = {http://www.sss.co.nz/},
year = 2008 
}

BACK TO INDEX

Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

The contents of this webpage is provided by the authors stated below. KU Leuven is not bound by the information provided. It is possible that the information is not or no longer completely accurate. Where necessary, the authors can adjust and update faulty information. The authors have taken all reasonable care to ensure that all information available on this website is accurate at the time of publication and on the basis of the current state of knowledge. KU Leuven nor the authors are responsible for the content of any links to external organisations that are referred to on this website.

Last modified: Mon Dec 16 13:19:46 2013
This bibliography was compiled by the following authors:

Peter Van Weert [home, mail]
Jon Sneyers [home, mail]
Tom Schrijvers [home, mail]
Leslie De Koninck

Please send BibT_EX entries of missing CHR-related publications to Jon Sneyers.

This document was translated from BibT_EX by bibtex2html