Publications of year 2007 (complete with abstract and BibTeX)

Publications of year 2007

Books and proceedings

V. Dahl and I. Niemelä, editors. ICLP '07: Proc. 23rd Intl. Conf. Logic Programming, volume 4670 of Lecture Notes in Computer Science, September 2007. Springer-Verlag. [doi:10.1007/978-3-540-74610-2]

@proceedings{piclp07,
title = ICLP07l,
booktitle = ICLP07,
editor = {Dahl, V. and Niemel\"a, I.},
series = LNCS,
volume = 4670,
doi = {10.1007/978-3-540-74610-2},
publisher = SV,
year = 2007,
month = sep,
location = {Porto, Portugal},
city = {Porto, Portugal},

}

K. Djelloul, G. J. Duck, and M. Sulzmann, editors. CHR '07: Proc. 4th Workshop on Constraint Handling Rules, September 2007. Keyword(s): CHR 2007.

@proceedings{pchr07,
title = CHR07l,
booktitle = CHR07,
year = {2007},
month = sep,
location = {Porto, Portugal},
city = {Porto, Portugal},
editor = {K. Djelloul and G. J. Duck and M. Sulzmann},
keywords = {CHR 2007},

}

M. Leuschel and A. Podelski, editors. PPDP '07: Proc. 9th Intl. Conf. Princ. Pract. Declarative Programming, July 2007. ACM Press. ISBN: 978-1-59593-769-8.

@proceedings{pppdp07,
title = PPDP07l,
booktitle = PPDP07,
editor = {M. Leuschel and A. Podelski},
publisher = ACM,
year = {2007},
month = jul,
location = {Wroc\l{}aw, Poland},
city = {Wroc\l{}aw, Poland},
isbn = {978-1-59593-769-8},

}

Articles in journal, book chapters

Marco Alberti, Federico Chesani, Davide Daolio, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. Specification and Verification of Agent Interaction Protocols in a Logic-based System. Scalable Computing: Practice and Experience, 8(1):1-13, March 2007. Abstract:

A number of information systems can be described as a set of interacting entities, which must follow interaction protocols. These protocols determine the behaviour and the properties of the overall system, hence it is of the uttermost importance that the entities behave in a conformant manner. A typical case is that of multi-agent systems, composed of a plurality of agents without a centralized control. Compliance to protocols can be hardwired in agent programs; however, this requires that only ``certified'' agents interact. In open systems, composed of autonomous and heterogeneous entities whose internal structure is, in general, not accessible (open agent societies being, again, a prominent example) interaction protocols should be specified in terms of the extit{observable} behaviour, and compliance should be verified by an external entity. In this paper, we propose a Java-Prolog-CHR system for verification of compliance of computational entities to protocols specified in a logic-based formalism ( extit{Social Integrity Constraints}). We also show the application of the formalism and the system to the specification and verification of three different scenarios: two specifications show the feasibility of our approach in the context of Multi Agent Systems (FIPA Contract-Net Protocol and Semi-Open societies), while a third specification applies to the specification of a lower level protocol (Open-Connection phase of the TCP protocol).

@article{alberti_et_al_agent_interaction_scpe07,
author = {Marco Alberti and Federico Chesani and Davide Daolio and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Specification and Verification of Agent Interaction Protocols in a Logic-based System},
journal = {Scalable Computing: Practice and Experience},
year = 2007,
volume = 8,
number = 1,
pages = {1--13},
month = mar,
abstract = { A number of information systems can be described as a set of interacting entities, which must follow interaction protocols. These protocols determine the behaviour and the properties of the overall system, hence it is of the uttermost importance that the entities behave in a conformant manner. 

A typical case is that of multi-agent systems, composed of a plurality of agents without a centralized control. Compliance to protocols can be hardwired in agent programs; however, this requires that only ``certified'' agents interact. In open systems, composed of autonomous and heterogeneous entities whose internal structure is, in general, not accessible (open agent societies being, again, a prominent example) interaction protocols should be specified in terms of the 	extit{observable} behaviour, and compliance should be verified by an external entity. 

In this paper, we propose a Java-Prolog-CHR system for verification of compliance of computational entities to protocols specified in a logic-based formalism (	extit{Social Integrity Constraints}). We also show the application of the formalism and the system to the specification and verification of three different scenarios: two specifications show the feasibility of our approach in the context of Multi Agent Systems (FIPA Contract-Net Protocol and Semi-Open societies), while a third specification applies to the specification of a lower level protocol (Open-Connection phase of the TCP protocol). },
publisher = {West University of Timisoara},

}

Mathieu Boespflug. TaiChi:how to check your types with serenity. The Monad.Reader, 9:17-31, November 2007. Keyword(s): type systems.

@article{boespflug_taichi_monadreader07,
author = {Mathieu Boespflug},
title = {{TaiChi:how to check your types with serenity}},
keywords = {type systems},
pages = {17--31},
journal = {The Monad.Reader},
volume = 9,
year = 2007,
month = nov 
}

Jacques Robin, Jairson Vitorino, and Armin Wolf. Constraint Programming Architectures: Review and a New Proposal. J. Universal Computer Science, 13(6):701-720, 2007. [WWW] Abstract:

Most automated reasoning tasks with prac tical applications can be automatically reformulated into a constraint solving task. A constraint programming platform can thus act as a unique, underlying engine to be reused for mu ltiple automated reasoning tasks in intelligent agents and systems. We identify six key requirements for such platform: expressive task modeling language, rapid solving method custom ization and combination, adaptive solving method, user-friendly solution explanation, efficient execution, and seamless integration within larger systems and practical applications. We then propose a novel, model-driven, component and rule-based architecture for such a platform that better satisfies as a whole this set of requirements than those of currently available platforms.

@article{robin_vitorino_wolf_CPA_proposal_jucs07,
author = {Jacques Robin and Jairson Vitorino and Armin Wolf},
title = {Constraint Programming Architectures: Review and a New Proposal},
journal = j-jucs,
volume = 13,
number = 6,
year = 2007,
pages = {701--720},
abstract = {Most automated reasoning tasks with prac tical applications can be automatically reformulated into a constraint solving task. A constraint programming platform can thus act as a unique, underlying engine to be reused for mu ltiple automated reasoning tasks in intelligent agents and systems. We identify six key requirements for such platform: expressive task modeling language, rapid solving method custom ization and combination, adaptive solving method, user-friendly solution explanation, efficient execution, and seamless integration within larger systems and practical applications. We then propose a novel, model-driven, component and rule-based architecture for such a platform that better satisfies as a whole this set of requirements than those of currently available platforms.},
url = {http://www.jucs.org/jucs_13_6/constraint_programming_architectures_review},

}

Beata Sarna-Starosta, R. E. Kurt Stirewalt, and Laura K. Dillon. A Model-Based Design-for-Verification Approach to Checking for Deadlock in Multi-Threaded Applications. Intl. Journal of Softw. Engin. and Knowl. Engin., 17(2):207-230, 2007. [doi:10.1142/S0218194007003197] Keyword(s): applications, testing. Abstract:

This paper explores an approach to design for verification in systems built atop a middleware framework which separates synchronization concerns from the ``core-functional logic'' of a program. The framework is based on a language-independent compositional model of synchronization contracts, called Szumo, which integrates well with popular OO design artifacts and provides strong guarantees of non-interference for a class of strictly exclusive systems. An approach for extracting models from Szumo design artifacts and analyzing the generated models to detect deadlocks is described. A key decision was to use Constraint Handling Rules to express the semantics of synchronization contracts, which allowed a transparent model of the implementation logic.

@article{ss_stirewalt_dillon_checking_deadlock_ijseke07,
author = {Beata Sarna-Starosta and R. E. Kurt Stirewalt and Laura K. Dillon},
title = {A Model-Based Design-for-Verification Approach to Checking for Deadlock in Multi-Threaded Applications},
keywords = {applications,testing},
journal = {Intl.\ Journal of Softw.\ Engin.\ and Knowl.\ Engin.},
volume = 17,
number = 2,
year = 2007,
pages = {207--230},
abstract = { This paper explores an approach to design for verification in systems built atop a middleware framework which separates synchronization concerns from the ``core-functional logic'' of a program. The framework is based on a language-independent compositional model of synchronization contracts, called Szumo, which integrates well with popular OO design artifacts and provides strong guarantees of non-interference for a class of strictly exclusive systems. An approach for extracting models from Szumo design artifacts and analyzing the generated models to detect deadlocks is described. A key decision was to use Constraint Handling Rules to express the semantics of synchronization contracts, which allowed a transparent model of the implementation logic. },
doi = {10.1142/S0218194007003197},

}

Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones, and Peter J. Stuckey. Understanding functional dependencies via Constraint Handling Rules. J. Functional Prog., 17(1):83-129, 2007. [doi:10.1017/S0956796806006137] Keyword(s): type systems.

@article{sulz_duck_peyton_stuck_func_dep_via_chr_fp07,
author = {Martin Sulzmann and Gregory J. Duck and Simon Peyton-Jones and Peter J. Stuckey},
title = {Understanding functional dependencies via {C}onstraint {H}andling {R}ules},
keywords = {type systems},
journal = {J. Functional Prog.},
volume = {17},
number = {1},
year = {2007},
pages = {83--129},
doi = {10.1017/S0956796806006137},
publisher = CUP,

}

Conference articles

Hariolf Betz. Relating Coloured Petri Nets to Constraint Handling Rules. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 33-47, September 2007. [PDF] Keyword(s): CHR 2007, related formalisms, CHR 2007, CHR 2007. Abstract:

Constraint Handling Rules (CHR) is a declarative rulebased concurrent committed-choice programming language. Petri nets are a well-known formalism for modeling and analysis of concurrent processes. We aim to develop a framework to exploit Petri nets as a tool for the modeling and analysis of CHR programs. In this paper, we show that place/transition nets can easily be embedded into CHR and we develop a translation of a significant segment of CHR into coloured Petri nets (CPN).

@inproceedings{betz_petri_nets_chr07,
author = {Hariolf Betz},
title = {Relating Coloured {Petri} Nets to {C}onstraint {H}andling {R}ules},
pages = {33--47},
crossref = {pchr07},
abstract = { Constraint Handling Rules (CHR) is a declarative rulebased concurrent committed-choice programming language. Petri nets are a well-known formalism for modeling and analysis of concurrent processes. We aim to develop a framework to exploit Petri nets as a tool for the modeling and analysis of CHR programs. In this paper, we show that place/transition nets can easily be embedded into CHR and we develop a translation of a significant segment of CHR into coloured Petri nets (CPN). },
pdf = PAPERSHOME # {chr2007/betz_petri_nets_chr07.pdf},
keywords = {CHR 2007, related formalisms},

}

Hariolf Betz and Thom Frühwirth. A Linear-Logic Semantics for Constraint Handling Rules with Disjunction. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 17-31, September 2007. [PDF] Keyword(s): CHR 2007, semantics, linear logic, CHR 2007, CHR 2007. Abstract:

We motivate and develop a linear logic declarative semantics for CHR^∨, an extension of the CHR programming language that integrates concurrent committed choice with backtrack search and a predefined underlying constraint handler. We show that our semantics maps each of these aspects of the language to a distinct aspect of linear logic. We show how we can use this semantics to reason about derivations in CHR^∨ and we present strong theorems concerning its soundness and completeness.

@inproceedings{betz_fru_linear_logic_chr_disj_chr07,
author = {Hariolf Betz and Thom Fr{\"u}hwirth},
title = {A Linear-Logic Semantics for {C}onstraint {H}andling {R}ules with Disjunction},
pages = {17--31},
crossref = {pchr07},
abstract = { We motivate and develop a linear logic declarative semantics for CHR$^\vee$, an extension of the CHR programming language that integrates concurrent committed choice with backtrack search and a predefined underlying constraint handler. We show that our semantics maps each of these aspects of the language to a distinct aspect of linear logic. We show how we can use this semantics to reason about derivations in CHR$^\vee$ and we present strong theorems concerning its soundness and completeness. },
pdf = PAPERSHOME # {chr2007/betz_fru_linear_logic_chr_disj_chr07.pdf},
keywords = {CHR 2007, semantics, linear logic},

}

Henning Christiansen and Christian Theil Have. From Use Cases to UML Class Diagrams using Logic Grammars and Constraints. In RANLP '07: Proc. Intl. Conf. Recent Adv. Nat. Lang. Processing, pages 128-132, September 2007. Keyword(s): applications, linguistics.

@inproceedings{christ_have_use_cases_to_uml_ranlp07,
title = {From Use Cases to {UML} Class Diagrams using Logic Grammars and Constraints},
author = {Henning Christiansen and Have, Christian Theil},
booktitle = {RANLP '07: Proc.\ Intl.\ Conf.\ Recent Adv.\ Nat.\ Lang.\ Processing},
month = sep,
year = 2007,
location = {Borovets, Bulgaria},
city = {Borovets, Bulgaria},
keywords = {applications, linguistics},
pages = {128--132},

}

Verónica Dahl and Baohua Gu. A CHRG Analysis of ambiguity in Biological Texts. In CSLP '07: Proc. 4th Intl. Workshop on Constraints and Language Processing, August 2007. Note: Extended Abstract. Keyword(s): linguistics, applications.

@inproceedings{dahl_gu_chrg_amb_bio_texts_cslp07,
author = {Ver{\'o}nica Dahl and Baohua Gu},
title = {A {CHRG} Analysis of ambiguity in Biological Texts},
note = {Extended Abstract},
booktitle = {CSLP '07: Proc.\ 4th Intl.\ Workshop on Constraints and Language Processing},
location = {Roskilde, Denmark},
city = {Roskilde, Denmark},
month = aug,
keywords = {linguistics, applications},
year = 2007,

}

Leslie De Koninck, Tom Schrijvers, and Bart Demoen. The Correspondence Between the Logical Algorithms Language and CHR. In V. Dahl and I. Niemelä, editors, ICLP '07: Proc. 23rd Intl. Conf. Logic Programming, volume 4670 of Lecture Notes in Computer Science, pages 209-223, September 2007. Springer-Verlag. [doi:10.1007/978-3-540-74610-2_15] Keyword(s): related formalisms.
```
@inproceedings{dekoninck_schr_demoen_la-chr_iclp07,
author = {De Koninck, Leslie and Schrijvers, Tom and Demoen, Bart},
title = {The Correspondence Between the {L}ogical {A}lgorithms Language and {CHR}},
pages = {209--223},
keywords = {related formalisms},
doi = {10.1007/978-3-540-74610-2_15},
crossref = {piclp07} 
}
```

Leslie De Koninck, Tom Schrijvers, and Bart Demoen. User-definable Rule Priorities for CHR. In M. Leuschel and A. Podelski, editors, PPDP '07: Proc. 9th Intl. Conf. Princ. Pract. Declarative Programming, pages 25-36, July 2007. ACM Press. ISBN: 978-1-59593-769-8. [doi:10.1145/1273920.1273924] Keyword(s): priorities.
```
@inproceedings{dekoninck_schr_demoen_chrrp_ppdp07,
author = {De Koninck, Leslie and Schrijvers, Tom and Demoen, Bart},
title = {User-definable Rule Priorities for {CHR}},
keywords = {priorities},
pages = {25--36},
doi = {10.1145/1273920.1273924},
crossref = {pppdp07} 
}
```

Leslie De Koninck and Jon Sneyers. Join Ordering for Constraint Handling Rules. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 107-121, September 2007. [PDF] Keyword(s): optimizing compilation, CHR 2007, CHR 2007, CHR 2007. Abstract:

Join ordering is the problem of finding cost optimal execution plans for matching multi-headed rules. In the context of Constraint Handling Rules, this topic has received limited attention so far, even though it is of great importance for efficient CHR execution. We present a formal cost model for joins and investigate the possibility of join optimization at runtime. We propose some heuristic approximations of the parameters of this cost model, for both the static and dynamic case. We discuss an O(n log n) optimization algorithm for the special case of acyclic join graphs. However, in general, join order optimization is an NP-complete problem. Finally, we identify some classes of cyclic join graphs that can be reduced to acyclic ones.

@inproceedings{dekoninck_sney_join_ordering_chr07,
author = {De Koninck, Leslie and Jon Sneyers},
title = {Join Ordering for {C}onstraint {H}andling {R}ules},
keywords = {optimizing compilation},
pages = {107--121},
crossref = {pchr07},
abstract = { Join ordering is the problem of finding cost optimal execution plans for matching multi-headed rules. In the context of Constraint Handling Rules, this topic has received limited attention so far, even though it is of great importance for efficient CHR execution. We present a formal cost model for joins and investigate the possibility of join optimization at runtime. We propose some heuristic approximations of the parameters of this cost model, for both the static and dynamic case. We discuss an O(n log n) optimization algorithm for the special case of acyclic join graphs. However, in general, join order optimization is an NP-complete problem. Finally, we identify some classes of cyclic join graphs that can be reduced to acyclic ones. },
pdf = PAPERSHOME # {chr2007/dekoninck_sney_join_ordering_chr07.pdf},
keywords = {CHR 2007},

}

Khalil Djelloul, Thi-Bich-Hanh Dao, and Thom Frühwirth. Toward a first-order extension of Prolog's unification using CHR: a CHR first-order constraint solver over finite or infinite trees. In SAC '07: Proc. 2007 ACM Symp. Applied computing, pages 58-64, 2007. ACM Press. ISBN: 1-59593-480-4.

@inproceedings{djelloul_dao_fru_1st_order_extension_prolog_unification_sac07,
author = {Khalil Djelloul and Thi-Bich-Hanh Dao and Thom Fr{\"u}hwirth},
title = {Toward a first-order extension of {P}rolog's unification using {CHR}: a {CHR} first-order constraint solver over finite or infinite trees},
booktitle = {SAC '07: Proc.\ 2007 ACM Symp.\ Applied computing},
year = {2007},
isbn = {1-59593-480-4},
pages = {58--64},
location = {Seoul, Korea},
city = {Seoul, Korea},
publisher = ACM,

}

Gregory J. Duck, Peter J. Stuckey, and Martin Sulzmann. Observable Confluence for Constraint Handling Rules. In V. Dahl and I. Niemelä, editors, ICLP '07: Proc. 23rd Intl. Conf. Logic Programming, volume 4670 of Lecture Notes in Computer Science, pages 224-239, September 2007. Springer-Verlag. [doi:10.1007/978-3-540-74610-2_16] Keyword(s): confluence.
```
@inproceedings{duck_stuck_sulz_observable_confluence_iclp07,
author = {Gregory J. Duck and Peter J. Stuckey and Martin Sulzmann},
title = {Observable Confluence for {C}onstraint {H}andling {R}ules},
pages = {224--239},
doi = {10.1007/978-3-540-74610-2_16},
keywords = {confluence},
crossref = {piclp07} 
}
```

Thom Frühwirth. Description Logic and Rules the CHR Way. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 49-61, September 2007. Note: Extended Abstract. [PDF] Keyword(s): related formalisms, CHR 2007, CHR 2007, CHR 2007. Abstract:

The challenges of the Semantic Web endeavour in knowledge representation and reasoning prompted a wealth of research in combining description logic (DL) as ontology languages (e.g. OWL) with logic programming for rule-based reasoning. General issues of combining and integrating formalisms have to be faced such as the type of combination, conceptual simplicity and tractability. Even though constraint-based programming has a tradition of tackling these questions, constraint-based rule formalisms such as constraint logic programming, concurrent constraint programming, constraint databases and constraint handling rules (CHR) have not explicitely been considered for combination with DL yet. The same holds for concurrency, which is an essential characteristic of the internet, but to the best of our knowledge has not been related to DL so far. Since CHR is a very expressive declarative concurrent constraintbased programming language with optimal performance guarantee and other interesting properties, we explore in this speculative paper what a CHR-based approach would look like in comparison to recent approaches for integrating OWL and rules.

@inproceedings{fru_description_logic_chr07,
author = {Thom Fr{\"u}hwirth},
title = {Description Logic and Rules the {CHR} Way},
pages = {49--61},
keywords = {related formalisms},
crossref = {pchr07},
abstract = { The challenges of the Semantic Web endeavour in knowledge representation and reasoning prompted a wealth of research in combining description logic (DL) as ontology languages (e.g. OWL) with logic programming for rule-based reasoning. General issues of combining and integrating formalisms have to be faced such as the type of combination, conceptual simplicity and tractability. Even though constraint-based programming has a tradition of tackling these questions, constraint-based rule formalisms such as constraint logic programming, concurrent constraint programming, constraint databases and constraint handling rules (CHR) have not explicitely been considered for combination with DL yet. The same holds for concurrency, which is an essential characteristic of the internet, but to the best of our knowledge has not been related to DL so far. Since CHR is a very expressive declarative concurrent constraintbased programming language with optimal performance guarantee and other interesting properties, we explore in this speculative paper what a CHR-based approach would look like in comparison to recent approaches for integrating OWL and rules. },
pdf = PAPERSHOME # {chr2007/fru_description_logic_chr07.pdf},
keywords = {CHR 2007},
note = {Extended Abstract},

}

Rémy Haemmerlé and François Fages. Abstract Critical Pairs and Confluence of Arbitrary Binary Relations. In RTA '07: Proc. 18th Intl. Conf. Term Rewriting and Applications, volume 4533 of Lecture Notes in Computer Science, June 2007. Springer-Verlag. [doi:10.1007/978-3-540-73449-9_17] Keyword(s): confluence. Abstract:

In a seminal paper, Huet introduced abstract properties of term rewriting systems, and the confluence analysis of terminating term rewriting systems by critical pairs computation. In this paper, we provide an abstract notion of critical pair for arbitrary binary relations and context operators. We show how this notion applies to the confluence analysis of various transition systems, ranging from classical term rewriting systems to production rules with constraints and partial control strategies, such as the Constraint Handling Rules language CHR. Interestingly, we show in all these cases that some classical critical pairs can be disregarded. The crux of these analyses is the ability to compute critical pairs between states built with general context operators, on which a bounded, not necessarily well-founded, ordering is assumed.

@inproceedings{haemm_fages_abstract_critical_pairs_rta07,
author = {R{\'e}my Haemmerl{\'e} and Fran{\c c}ois Fages},
title = {Abstract Critical Pairs and Confluence of Arbitrary Binary Relations},
booktitle = {RTA '07: Proc.\ 18th Intl.\ Conf.\ Term Rewriting and Applications},
location = {Paris, France},
city = {Paris, France},
year = 2007,
month = jun,
publisher = SV,
series = LNCS,
volume = 4533,
keywords = {confluence},
doi = {10.1007/978-3-540-73449-9_17},
abstract = {In a seminal paper, Huet introduced abstract properties of term rewriting systems, and the confluence analysis of terminating term rewriting systems by critical pairs computation. In this paper, we provide an abstract notion of critical pair for arbitrary binary relations and context operators. We show how this notion applies to the confluence analysis of various transition systems, ranging from classical term rewriting systems to production rules with constraints and partial control strategies, such as the Constraint Handling Rules language CHR. Interestingly, we show in all these cases that some classical critical pairs can be disregarded. The crux of these analyses is the ability to compute critical pairs between states built with general context operators, on which a bounded, not necessarily well-founded, ordering is assumed.},

}

Ben Krause and Tim Wahls. jmle: A Tool for Executing JML Specifications via Constraint Programming. In Formal Methods: Applications and Technology, volume 4346 of Lecture Notes in Computer Science, pages 293-296, 2007. Springer-Verlag. [doi:10.1007/978-3-540-70952-7_19] Abstract:

Formal specifications are more useful and easier to develop if they are executable. In this work, we describe a system for executing specifications written in the Java Modeling Language (JML) by translating them to constraint programs, which are then executed via the Java Constraint Kit (JCK). Our system can execute specifications written at a high level of abstraction, and the generated constraint programs are Java implementations of the translated specifications. Hence, they can be called directly from ordinary Java code.

@inproceedings{krause_wahls_jmle_fmics06,
author = {Ben Krause and Tim Wahls},
title = {jmle: A Tool for Executing JML Specifications via Constraint Programming},
booktitle = {Formal Methods: Applications and Technology},
series = LNCS,
volume = 4346,
year = 2007,
abstract = { Formal specifications are more useful and easier to develop if they are executable. In this work, we describe a system for executing specifications written in the Java Modeling Language (JML) by translating them to constraint programs, which are then executed via the Java Constraint Kit (JCK). Our system can execute specifications written at a high level of abstraction, and the generated constraint programs are Java implementations of the translated specifications. Hence, they can be called directly from ordinary Java code. },
pages = {293--296},
publisher = SV,
doi = {10.1007/978-3-540-70952-7_19},

}

Edmund S.L. Lam and Martin Sulzmann. A Concurrent Constraint Handling Rules Semantics and its Implementation with Software Transactional Memory. In DAMP '07: Proc. ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, January 2007. ACM Press. [WWW] Keyword(s): parallelism.

@inproceedings{lam_sulz_concurrent_chr_damp07,
title = {A Concurrent {C}onstraint {H}andling {R}ules Semantics and its Implementation with Software Transactional Memory},
author = {Edmund S.L. Lam and Martin Sulzmann},
keywords = {parallelism},
booktitle = {DAMP '07: Proc.\ ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming},
month = jan,
year = 2007,
location = {Nice, France},
city = {Nice, France},
url = {http://taichi.ddns.comp.nus.edu.sg/taichiwiki/CCHR/},
publisher = ACM,

}

Martin Magnusson and Patrick Doherty. Deductive Planning with Temporal Constraints. In Eyal Amir, Vladimir Lifschitz, and Rob Miller, editors, Logical Formalizations of Commonsense Reasoning: Papers from the 2007 AAAI Spring Symposium, March 2007. AAAI Press.

@inproceedings{magnusson_doherty_deductive_planning_aaai07,
author = {Martin Magnusson and Patrick Doherty},
title = {Deductive Planning with Temporal Constraints},
editor = {Eyal Amir and Vladimir Lifschitz and Rob Miller},
booktitle = {Logical Formalizations of Commonsense Reasoning: Papers from the 2007 AAAI Spring Symposium},
location = {Stanford, California},
month = {March},
year = {2007},
publisher = {AAAI Press} 
}

Julien Martin and François Fages. From Business Rules to Constraint Programs in Warehouse Management Systems. In Doctoral programme of the 13th Intl. Conf. on Princ. and Pract. of Constraint Programming, 2007. Keyword(s): related formalisms.

@inproceedings{martin_fages_business_rules_cpdc07,
author = {Julien Martin and Fran{\c c}ois Fages},
title = {From Business Rules to Constraint Programs in Warehouse Management Systems},
keywords = {related formalisms},
booktitle = {Doctoral programme of the 13th Intl.\ Conf.\ on Princ.\ and Pract.\ of Constraint Programming},
year = 2007,

}

Marc Meister. Concurrency of the preflow-push algorithm in Constraint Handling Rules. In CSCLP'07: Proc. 12th Intl. Workshop on Constraint Solving and Constraint Logic Programming, pages 160-169, 2007. Keyword(s): algorithms, parallelism.

@inproceedings{meister_preflowpush_csclp07,
author = {Marc Meister},
title = {Concurrency of the preflow-push algorithm in {C}onstraint {H}andling {R}ules},
keywords = {algorithms, parallelism},
booktitle = {CSCLP'07: Proc. 12th Intl. Workshop on Constraint Solving and Constraint Logic Programming},
location = {Rocquencourt, France},
city = {Rocquencourt, France},
pages = {160--169},
year = 2007,

}

Marc Meister, Khalil Djelloul, and Jacques Robin. A Unified Semantics for Constraint Handling Rules in Transaction Logic. In C. Baral, G. Brewka, and J. S. Schlipf, editors, LPNMR '07: Proc. 9th Intl. Conf. Logic Programming and Nonmonotonic Reasoning, volume 4483 of Lecture Notes in Computer Science, pages 201-213, May 2007. Springer-Verlag. [doi:10.1007/978-3-540-72200-7_18] Keyword(s): semantics.

@InProceedings{meister_djelloul_robin_transaction_logic_semantics_lpnmr07,
title = "A Unified Semantics for {C}onstraint {H}andling {R}ules in Transaction Logic",
author = "Marc Meister and Khalil Djelloul and Jacques Robin",
keywords = {semantics},
booktitle = "LPNMR '07: Proc.\ 9th Intl.\ Conf.\ Logic Programming and Nonmonotonic Reasoning",
location = {Tempe, AZ, USA},
city = {Tempe, AZ, USA},
month = may,
publisher = SV,
year = "2007",
volume = "4483",
editor = "C. Baral and G. Brewka and J. S. Schlipf",
pages = "201--213",
series = LNCS,
doi = "10.1007/978-3-540-72200-7_18",

}

Paolo Pilozzi, Tom Schrijvers, and Danny De Schreye. Proving termination of CHR in Prolog: A transformational approach. In WST '07: 9th Intl. Workshop on Termination, June 2007. Keyword(s): termination.

@inproceedings{pilozzi_schr_deschreye_termination_wst07,
author = {Paolo Pilozzi and Tom Schrijvers and Danny {De Schreye}},
title = { Proving termination of {CHR} in {Prolog}: A transformational approach },
booktitle = {WST '07: 9th Intl.\ Workshop on Termination},
month = jun,
year = 2007,
location = {Paris, France},
city = {Paris, France},
keywords = {termination} 
}

Frank Raiser. Graph Transformation Systems in CHR. In V. Dahl and I. Niemelä, editors, ICLP '07: Proc. 23rd Intl. Conf. Logic Programming, volume 4670 of Lecture Notes in Computer Science, pages 240-254, September 2007. Springer-Verlag. [doi:10.1007/978-3-540-74610-2_17] Keyword(s): Graph Transformation Systems, related formalisms.
```
@inproceedings{raiser_graph_transformation_systems_iclp07,
author = {Frank Raiser},
title = {Graph Transformation Systems in {CHR}},
keywords = {Graph Transformation Systems, related formalisms},
pages = {240--254},
doi = {10.1007/978-3-540-74610-2_17},
crossref = {piclp07} 
}
```

Frank Raiser and Paolo Tacchella. On Confluence of Non-terminating CHR Programs. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 63-76, September 2007. [PDF] Keyword(s): CHR 2007, confluence, CHR 2007, CHR 2007. Abstract:

Confluence is an important property for any kind of rewrite system including CHR, which is a general-purpose declarative committedchoice language consisting of multi-headed guarded rules. CHR can yield a confluence problem, because of non-determinism in the choice of rules using the abstract semantics. Confluence in CHR is an ongoing research topic, because it provides numerous benefits for implementations. However, for non-terminating CHR programs confluence is generally undecidable. In this paper we apply the so-called Strong Church-Rosser property to CHR. This allows determination of confluence for a subset of non-terminating CHR programs.

@inproceedings{raiser_tacchella_confluence_non_terminating_chr07,
author = {Frank Raiser and Paolo Tacchella},
title = {On Confluence of Non-terminating {CHR} Programs},
pages = {63--76},
crossref = {pchr07},
abstract = { Confluence is an important property for any kind of rewrite system including CHR, which is a general-purpose declarative committedchoice language consisting of multi-headed guarded rules. CHR can yield a confluence problem, because of non-determinism in the choice of rules using the abstract semantics. Confluence in CHR is an ongoing research topic, because it provides numerous benefits for implementations. However, for non-terminating CHR programs confluence is generally undecidable. In this paper we apply the so-called Strong Church-Rosser property to CHR. This allows determination of confluence for a subset of non-terminating CHR programs. },
pdf = PAPERSHOME # {chr2007/raiser_tacchella_confluence_non_terminating_chr07.pdf},
keywords = {CHR 2007, confluence},

}

Beata Sarna-Starosta and C.R. Ramakrishnan. Compiling Constraint Handling Rules for Efficient Tabled Evaluation. In M. Hanus, editor, PADL '07: Proc. 9th Intl. Symp. Practical Aspects of Declarative Languages, volume 4354 of Lecture Notes in Computer Science, pages 170-184, January 2007. Springer-Verlag. [doi:10.1007/978-3-540-69611-7_11] Keyword(s): implementation.

@inproceedings{sarnastarosta_ramakrishnan_chrd_padl07,
author = {Beata Sarna-Starosta and C.R. Ramakrishnan},
title = {Compiling {C}onstraint {H}andling {R}ules for Efficient Tabled Evaluation},
keywords = {implementation},
pages = {170--184},
booktitle = {PADL '07: Proc.\ 9th Intl.\ Symp.\ Practical Aspects of Declarative Languages},
editor = {M. Hanus},
location = {Nice, France},
city = {Nice, France},
month = jan,
year = 2007,
publisher = SV,
series = LNCS,
volume = 4354,
doi = {10.1007/978-3-540-69611-7_11},

}

Stephan Schiffel and Michael Thielscher. Fluxplayer: A Successful General Game Player. In AAAI '07: Proc. 22nd AAAI Conf. Artificial Intelligence, pages 1191-1196, July 2007. AAAI Press. Keyword(s): FLUX.

@inproceedings{schiffel_thielscher_fluxplayer_aaai07,
author = {Stephan Schiffel and Michael Thielscher},
title = {Fluxplayer: A Successful General Game Player},
keywords = {FLUX},
year = {2007},
pages = {1191--1196},
booktitle = {AAAI '07: Proc. 22nd AAAI Conf. Artificial Intelligence},
month = jul,
location = {Vancouver, Canada},
city = {Vancouver, Canada},
publisher = {AAAI Press},

}

Jon Sneyers, Peter Van Weert, and Tom Schrijvers. Aggregates for Constraint Handling Rules. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 91-105, September 2007. [PDF] Keyword(s): CHR 2007, extensions, CHR 2007, CHR 2007. Abstract:

We extend the Constraint Handling Rules language with aggregates such as sum, count, findall, and min. The proposed extension features nested aggregate expressions over guarded conjunctions of constraints, a series of predefined aggregates, and application-tailored user-defined aggregates. We formally define the operational semantics of aggregates, and show how incremental aggregate computation facilitates efficient implementations. Case studies demonstrate that language support for aggregates significantly reduces program size, thus improving readability and maintainability considerably.

@inproceedings{sney_vanweert_demoen_aggregates_chr07,
author = {Jon Sneyers and Van Weert, Peter and Tom Schrijvers},
title = {Aggregates for {C}onstraint {H}andling {R}ules},
pages = {91--105},
crossref = {pchr07},
abstract = { We extend the Constraint Handling Rules language with aggregates such as sum, count, findall, and min. The proposed extension features nested aggregate expressions over guarded conjunctions of constraints, a series of predefined aggregates, and application-tailored user-defined aggregates. We formally define the operational semantics of aggregates, and show how incremental aggregate computation facilitates efficient implementations. Case studies demonstrate that language support for aggregates significantly reduces program size, thus improving readability and maintainability considerably. },
pdf = PAPERSHOME # {chr2007/sney_vanweert_demoen_aggregates_chr07.pdf},
keywords = {CHR 2007, extensions},

}

Jon Sneyers, Peter Van Weert, Tom Schrijvers, and Bart Demoen. Aggregates in Constraint Handling Rules: Extended Abstract. In V. Dahl and I. Niemelä, editors, ICLP '07: Proc. 23rd Intl. Conf. Logic Programming, volume 4670 of Lecture Notes in Computer Science, pages 446-448, September 2007. Springer-Verlag. [doi:10.1007/978-3-540-74610-2_39] Keyword(s): extensions.
```
@inproceedings{sney_vanweert_schr_demoen_aggregates_iclp07,
author = {Jon Sneyers and Van Weert, Peter and Tom Schrijvers and Bart Demoen},
title = {Aggregates in {C}onstraint {H}andling {R}ules: Extended Abstract},
pages = {446--448},
doi = {10.1007/978-3-540-74610-2_39},
keywords = {extensions},
crossref = {piclp07} 
}
```

Martin Sulzmann and Edmund S.L. Lam. Compiling Constraint Handling Rules with Lazy and Concurrent Search Techniques. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 139-149, September 2007. [PDF] Keyword(s): CHR 2007, parallelism, CHR 2007, CHR 2007. Abstract:

Constraint Handling Rules (CHR) is a concurrent commited choice constraint programming language to describe transformations (rewritings) among multi-sets of constraints. One of the main CHR execution tasks is the search for constraints matching a rule head. Several optimization techniques have been widely studied, yet the actual details of the search strategies and their implementation are rarely the center of attention. In this paper, we explore the implementation of several search strategies using the lazy functional language Haskell. In combination with concurrency abstractions as supported by the Glasgow Haskell Compiler we obtain very clean and efficient implementations for searching of matching constraints.

@inproceedings{sulz_lam_lazy_concurr_search_chr07,
title = {Compiling {C}onstraint {H}andling {R}ules with Lazy and Concurrent Search Techniques},
author = {Martin Sulzmann and Edmund S.L. Lam},
pages = {139--149},
crossref = {pchr07},
abstract = { Constraint Handling Rules (CHR) is a concurrent commited choice constraint programming language to describe transformations (rewritings) among multi-sets of constraints. One of the main CHR execution tasks is the search for constraints matching a rule head. Several optimization techniques have been widely studied, yet the actual details of the search strategies and their implementation are rarely the center of attention. In this paper, we explore the implementation of several search strategies using the lazy functional language Haskell. In combination with concurrency abstractions as supported by the Glasgow Haskell Compiler we obtain very clean and efficient implementations for searching of matching constraints. },
pdf = PAPERSHOME # {chr2007/sulz_lam_lazy_concurr_search_chr07.pdf},
keywords = {CHR 2007, parallelism},

}

Martin Sulzmann and Edmund S.L. Lam. Haskell - Join - Rules. In Olaf Chitil, editor, IFL '07: 19th Intl. Symp. Implementation and Application of Functional Languages, pages 195-210, September 2007. Keyword(s): related formalisms.

@inproceedings{sulz_lam_haskelljoinrules_ifl07,
title = {{Haskell - Join - Rules}},
keywords = {related formalisms},
author = {Martin Sulzmann and Edmund S.L. Lam},
editor = {Olaf Chitil},
booktitle = {IFL '07: 19th Intl.\ Symp.\ Implementation and Application of Functional Languages},
pages = {195--210},
year = 2007,
month = sep,
location = {Freiburg, Germany},
city = {Freiburg, Germany},

}

Martin Sulzmann and Meng Wang. Aspect-oriented programming with type classes. In Proceedings of the 6th workshop on Foundations of aspect-oriented languages, FOAL '07, pages 65-74, 2007. ACM. ISBN: 978-1-59593-671-4. [WWW] Keyword(s): type systems.

@inproceedings{Sulzmann:2007:APT:1233833.1233842,
author = {Sulzmann, Martin and Wang, Meng},
title = {Aspect-oriented programming with type classes},
booktitle = {Proceedings of the 6th workshop on Foundations of aspect-oriented languages},
series = {FOAL '07},
year = {2007},
isbn = {978-1-59593-671-4},
location = {Vancouver, British Columbia, Canada},
pages = {65--74},
url = {http://doi.acm.org/10.1145/1233833.1233842},
publisher = {ACM},
keywords = {type systems},

}

Paolo Tacchella, Maurizio Gabbrielli, and Maria Chiara Meo. Unfolding in CHR. In M. Leuschel and A. Podelski, editors, PPDP '07: Proc. 9th Intl. Conf. Princ. Pract. Declarative Programming, pages 179-186, July 2007. ACM Press. ISBN: 978-1-59593-769-8.
```
@inproceedings{tacchella_gabbrielli_meo_unfolding_ppdp07,
author = {Paolo Tacchella and Maurizio Gabbrielli and Maria Chiara Meo},
title = {Unfolding in {CHR}},
pages = {179--186},
crossref = {pppdp07} 
}
```

Dean Voets, Paolo Pilozzi, and Danny De Schreye. A new approach to termination analysis of Constraint Handling Rules. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 77-89, September 2007. [PDF] Keyword(s): CHR 2007, termination, CHR 2007, CHR 2007. Abstract:

We present a new approach to termination analysis of Constraint Handling Rules. The approach, compared to existing approaches, is applicable to a much larger class of CHR programs. A new termination condition is formulated, that instead of a termination argument based on the comparison of sizes of consecutive computation states, verifies conditions imposed on the dynamic process of adding constraints to the store. The condition's applicability to CHR programs, with rules not only of the simplification type, has been successfully tested, using a semi-automated analyzer.

@inproceedings{voets_pilozzi_deschreye_termination_chr07,
author = {Dean Voets and Paolo Pilozzi and Danny {De Schreye}},
title = {A new approach to termination analysis of {C}onstraint {H}andling {R}ules},
pages = {77--89},
crossref = {pchr07},
abstract = { We present a new approach to termination analysis of Constraint Handling Rules. The approach, compared to existing approaches, is applicable to a much larger class of CHR programs. A new termination condition is formulated, that instead of a termination argument based on the comparison of sizes of consecutive computation states, verifies conditions imposed on the dynamic process of adding constraints to the store. The condition's applicability to CHR programs, with rules not only of the simplification type, has been successfully tested, using a semi-automated analyzer. },
pdf = PAPERSHOME # {chr2007/voets_pilozzi_deschreye_termination_chr07.pdf},
keywords = {CHR 2007, termination},

}

Armin Wolf, Jacques Robin, and Jairson Vitorino. Adaptive CHR meets CHR^∨: An Extended Refined Operational Semantics for CHR^∨ Based On Justifications. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 1-15, September 2007. [PDF] Keyword(s): semantics, disjunction, CHR 2007, CHR 2007, CHR 2007. Abstract:

Adaptive constraint processing with Constraint Handling Rules (CHR) allows the application of intelligent search strategies to solve Constraint Satisfaction Problems (CSP), but these search algorithms have to be implemented in the host language of adaptive CHR, which is currently Java. On the other hand, CHR^∨ enables to explicitly formulate search in CHR, using disjunctive bodies to model choices. However, a naive implementation for handling disjunctions, in particular chronological backtracking (as implemented in Prolog) might cause "thrashing" due to an inappropriate order of decisions. To avoid this, a first combination of adaptive CHR and CHR^∨ is presented to offer a more efficient embedded search mechanism to handle disjunctions. Therefore the refined operational semantics of CHR is extended for disjunctions and adaptation.

@inproceedings{wolf_robin_vitorino_adaptive_chr_or_chr07,
author = {Armin Wolf and Jacques Robin and Jairson Vitorino},
title = {Adaptive {CHR} meets {CHR}$^{\lor}$: An Extended Refined Operational Semantics for {CHR}$^{\lor}$ Based On Justifications},
keywords = {semantics, disjunction},
pages = {1--15},
crossref = {pchr07},
abstract = { Adaptive constraint processing with Constraint Handling Rules (CHR) allows the application of intelligent search strategies to solve Constraint Satisfaction Problems (CSP), but these search algorithms have to be implemented in the host language of adaptive CHR, which is currently Java. On the other hand, CHR$^\vee$ enables to explicitly formulate search in CHR, using disjunctive bodies to model choices. However, a naive implementation for handling disjunctions, in particular chronological backtracking (as implemented in Prolog) might cause "thrashing" due to an inappropriate order of decisions. To avoid this, a first combination of adaptive CHR and CHR$^\vee$ is presented to offer a more efficient embedded search mechanism to handle disjunctions. Therefore the refined operational semantics of CHR is extended for disjunctions and adaptation. },
pdf = PAPERSHOME # {chr2007/wolf_robin_vitorino_adaptive_chr_or_chr07.pdf},
keywords = {CHR 2007},

}

Pieter Wuille, Tom Schrijvers, and Bart Demoen. CCHR: the fastest CHR Implementation, in C. In K. Djelloul, G. J. Duck, and M. Sulzmann, editors, CHR '07: Proc. 4th Workshop on Constraint Handling Rules, pages 123-137, September 2007. [WWW] [PDF] Keyword(s): CHR 2007, implementation, CHR 2007, CHR 2007. Abstract:

CHR is usually compiled to high-level languages (like Prolog) that make it hard or impossible to express low-level optimizations. This is a pity, because it confines CHR to be a prototyping language only, with an unacceptable performance for production quality software. This paper presents CCHR, a CHR system embedded in the C programming language, that compiles to low-level C code which is highly suitable for fine-grained performance improvements. In this way CCHR program performance comes close to matching that of native C, and easily outperforms other CHR implementations.

@inproceedings{wuille_schr_demoen_cchr_chr07,
author = {Pieter Wuille and Tom Schrijvers and Bart Demoen},
title = {{CCHR}: the fastest {CHR} Implementation, in {C}},
pages = {123--137},
crossref = {pchr07},
url = {http://people.cs.kuleuven.be/~pieter.wuille/CCHR/},
abstract = { CHR is usually compiled to high-level languages (like Prolog) that make it hard or impossible to express low-level optimizations. This is a pity, because it confines CHR to be a prototyping language only, with an unacceptable performance for production quality software. This paper presents CCHR, a CHR system embedded in the C programming language, that compiles to low-level C code which is highly suitable for fine-grained performance improvements. In this way CCHR program performance comes close to matching that of native C, and easily outperforms other CHR implementations. },
pdf = PAPERSHOME # {chr2007/wuille_schr_demoen_cchr_chr07.pdf},
keywords = {CHR 2007, implementation},

}

Internal reports

Leslie De Koninck, Tom Schrijvers, and Bart Demoen. CHR^rp: Constraint Handling Rules with rule priorties. Technical report CW 479, K.U.Leuven, Department of Computer Science, Leuven, Belgium, March 2007. [WWW] Keyword(s): priorities. Abstract:

We extend the Constraint Handling Rules language (CHR) with user-defined rule priorities. This language extension reduces the level of non-determinism that is inherent to the theoretical operational semantics of CHR, and gives a more high-level form of execution control compared to the refined operational semantics. We suggest some application areas. A formal operational semantics for the extended language, called CHR-rp, is given and its theoretical properties are discussed. We look at some issues with CHR-rp and discuss alternatives for rule priorities.

@techreport{dekoninck_schr_demoen_chrrp_techrep07,
author= {De Koninck, Leslie and Schrijvers, Tom and Demoen, Bart},
title = {CHR$^\mathrm{rp}$: {C}onstraint {H}andling {R}ules with rule priorties},
institution = KULCW,
address = {Leuven, Belgium},
year = {2007},
month = mar,
number = {CW 479},
keywords = {priorities},
abstract = { We extend the Constraint Handling Rules language (CHR) with user-defined rule priorities. This language extension reduces the level of non-determinism that is inherent to the theoretical operational semantics of CHR, and gives a more high-level form of execution control compared to the refined operational semantics. We suggest some application areas. A formal operational semantics for the extended language, called CHR-rp, is given and its theoretical properties are discussed. We look at some issues with CHR-rp and discuss alternatives for rule priorities. },
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW479.abs.html},

}

Leslie De Koninck, Tom Schrijvers, and Bart Demoen. The Correspondence Between the Logical Algorithms Language and CHR. Technical report CW 480, K.U.Leuven, Department of Computer Science, Leuven, Belgium, March 2007. [WWW] Keyword(s): related formalisms, priorities. Abstract:

This paper investigates the relationship between the Logical Algorithms language (LA) of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation scheme from LA to CHR-rp: CHR with rule priorities and show that the meta-complexity theorem for LA can be applied to a subset of CHR-rp via inverse translation. This result is compared with previous work. Inspired by the high-level implementation proposal of Ganzinger and McAllester, we demonstrate how LA programs can be compiled into CHR rules that interact with a scheduler written in CHR. This forms the first actual implementation of LA. Our implementation achieves the complexity required for the meta-complexity theorem to hold and can execute a subset of CHR-rp with strong complexity bounds.

@techreport{dekoninck_schr_demoen_la-chr_techrep07,
author = {De Koninck, Leslie and Schrijvers, Tom and Demoen, Bart},
title = {The Correspondence Between the {L}ogical {A}lgorithms Language and {CHR}},
institution = KULCW,
address = {Leuven, Belgium},
year = {2007},
month = mar,
number = {CW 480},
abstract = { This paper investigates the relationship between the Logical Algorithms language (LA) of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation scheme from LA to CHR-rp: CHR with rule priorities and show that the meta-complexity theorem for LA can be applied to a subset of CHR-rp via inverse translation. This result is compared with previous work. Inspired by the high-level implementation proposal of Ganzinger and McAllester, we demonstrate how LA programs can be compiled into CHR rules that interact with a scheduler written in CHR. This forms the first actual implementation of LA. Our implementation achieves the complexity required for the meta-complexity theorem to hold and can execute a subset of CHR-rp with strong complexity bounds. },
keywords = {related formalisms, priorities},
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW480.abs.html},

}

Leslie De Koninck, Peter J. Stuckey, and Gregory J. Duck. Optimized compilation of CHR^rp. Technical report CW 499, K.U.Leuven, Department of Computer Science, Leuven, Belgium, August 2007. [WWW] Keyword(s): implementation, optimizing compilation, priorities. Abstract:

Constraint Handling Rules were recently extended with user-definable rule priorities. This paper shows how this extended language can be efficiently compiled into the underlying host language. It extends previous work by supporting rules with a dynamic priority and by introducing various optimizations. The effects of the optimizations are empirically evaluated and the new compiler is compared with the state-of-the-art K.U.Leuven CHR system.

@techreport{dekoninck_stuck_duck_compiling-chrrp_techrep07,
author = {De Koninck, Leslie and Stuckey, Peter J. and Duck, Gregory J.},
title = {Optimized compilation of CHR$^\mathrm{rp}$},
keywords = {implementation, optimizing compilation, priorities},
institution = KULCW,
address = {Leuven, Belgium},
year = {2007},
month = aug,
number = {CW 499},
abstract = { Constraint Handling Rules were recently extended with user-definable rule priorities. This paper shows how this extended language can be efficiently compiled into the underlying host language. It extends previous work by supporting rules with a dynamic priority and by introducing various optimizations. The effects of the optimizations are empirically evaluated and the new compiler is compared with the state-of-the-art K.U.Leuven CHR system. },
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW499.abs.html},

}

Paolo Pilozzi, Tom Schrijvers, and Danny De Schreye. Proving termination of CHR in Prolog: A transformational approach. Technical report CW 487, K.U.Leuven, Department of Computer Science, Leuven, Belgium, April 2007. [WWW] Keyword(s): termination. Abstract:

In this paper we present a termination preserving transformation from Constraint Handling Rules to Prolog. The transformation is sound w.r.t. termination under the theoretical semantics of Constraint Handling Rules. It does not consider the presence of a propagation history. The transformation allows for the direct reuse of termination proof methods from Logic Programs and Term-Rewrite Systems, yielding the first fully automatic termination proving for Constraint Handling Rules. We formalize the transformation and show usefulness of the approach. We transform a set of CHR programs, by an implementation of the transformation and show termination by using existing termination tools for Logic Programs and Term-Rewrite Systems.

@techreport{pilozzi_schr_deschreye_termination_techrep07,
author = {Paolo Pilozzi and Tom Schrijvers and Danny {De Schreye}},
title = { Proving termination of {CHR} in {Prolog}: A transformational approach },
institution = KULCW,
address = {Leuven, Belgium},
year = {2007},
month = apr,
number = {CW 487},
abstract = { In this paper we present a termination preserving transformation from Constraint Handling Rules to Prolog. The transformation is sound w.r.t. termination under the theoretical semantics of Constraint Handling Rules. It does not consider the presence of a propagation history. The transformation allows for the direct reuse of termination proof methods from Logic Programs and Term-Rewrite Systems, yielding the first fully automatic termination proving for Constraint Handling Rules. We formalize the transformation and show usefulness of the approach. We transform a set of CHR programs, by an implementation of the transformation and show termination by using existing termination tools for Logic Programs and Term-Rewrite Systems. },
keywords = {termination},
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW487.abs.html},

}

Beata Sarna-Starosta and Tom Schrijvers. Indexing techniques for CHR based on program transformation. Technical report CW 500, K.U.Leuven, Department of Computer Science, Leuven, Belgium, August 2007. [WWW] Keyword(s): implementation, optimizing compilation. Abstract:

Multi-headed rules are essential for the expressiveness of CHR, but incur a considerable performance penalty. Current indexing techniques are often unable to address this problem. They are effective only when matchings have a particular form, or offer good run-time complexity rather than good absolute figures. In this paper we describe three advanced indexing techniques: (1) two program transformations that make other indexing techniques more effective, (2) an index for ground terms more efficient than hash tables, and (3) a post-processing program transformation that eliminates runtime overhead of (1) and (2). We compare these techniques with the current state of the art, and give measurements of their effectiveness in K.U.Leuven CHR and CHRd.

@techreport{sarnastarosta_schr_indexing_techrep07,
author = {Beata Sarna-Starosta and Tom Schrijvers},
title = {Indexing techniques for {CHR} based on program transformation},
institution = KULCW,
address = {Leuven, Belgium},
keywords = {implementation, optimizing compilation},
year = {2007},
month = aug,
number = {CW 500},
abstract = { Multi-headed rules are essential for the expressiveness of CHR, but incur a considerable performance penalty. Current indexing techniques are often unable to address this problem. They are effective only when matchings have a particular form, or offer good run-time complexity rather than good absolute figures. In this paper we describe three advanced indexing techniques: (1) two program transformations that make other indexing techniques more effective, (2) an index for ground terms more efficient than hash tables, and (3) a post-processing program transformation that eliminates runtime overhead of (1) and (2). We compare these techniques with the current state of the art, and give measurements of their effectiveness in K.U.Leuven CHR and CHRd. },
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW500.abs.html},

}

Jon Sneyers, Peter Van Weert, Tom Schrijvers, and Bart Demoen. Aggregates in CHR. Technical report CW 481, K.U.Leuven, Department of Computer Science, Leuven, Belgium, March 2007. [WWW] Keyword(s): extensions. Abstract:

We propose an extension of the Constraint Handling Rules language with aggregates like sum, count, findall, and min in the heads of rules. We define the semantics of aggregate expressions formally and informally. Our prototype implementation as a source-to-source preprocessor allows both on-demand and incremental computation of nested aggregate expressions over guarded conjunctions of constraints. Case studies demonstrate that by using aggregates, the program size can be significantly reduced, with only a small constant run-time overhead.

@techreport{sneyers_vanweert_et_al_aggregates_techrep07,
author = {Sneyers, Jon and Van Weert, Peter and Schrijvers, Tom and Demoen, Bart},
title = {Aggregates in {CHR}},
institution = KULCW,
address = {Leuven, Belgium},
year = {2007},
month = mar,
number = {CW 481},
keywords = {extensions},
abstract = { We propose an extension of the Constraint Handling Rules language with aggregates like sum, count, findall, and min in the heads of rules. We define the semantics of aggregate expressions formally and informally. Our prototype implementation as a source-to-source preprocessor allows both on-demand and incremental computation of nested aggregate expressions over guarded conjunctions of constraints. Case studies demonstrate that by using aggregates, the program size can be significantly reduced, with only a small constant run-time overhead. },
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW481.abs.html},

}

Miscellaneous

Martin Magnusson. Deductive Planning and Composite Actions in Temporal Action Logic. Master's thesis, Department of Computer and Information Science, Linköping University, Sweden, 2007. Note: Thesis No. 1329.

@mastersthesis{magnusson_deductive_planning_07,
title = {Deductive Planning and Composite Actions in Temporal Action Logic},
author = {Martin Magnusson},
school = {Department of Computer and Information Science, Link{\"o}ping University, Sweden},
year = {2007},
note = {Thesis No. 1329} 
}

Ersha Rahimikia. Detecting non-termination in Constraint Handling Rules. Master's thesis, Dept. Computing and Software, McMaster University, 2007. Keyword(s): termination, termination.

@mastersthesis{rahimikia_nontermination_msthesis07,
author = {Rahimikia, Ersha},
title = {Detecting non-termination in {C}onstraint {H}andling {R}ules},
keywords = {termination},
school = {Dept.\ Computing and Software, McMaster University},
year = 2007,
keywords = {termination},

}

Gerrit van den Geest. Constraints for Type Class Extensions. Master's thesis, Utrecht University, April 2007. Keyword(s): type systems.

@mastersthesis{gvdg_type_class_extensions_mthesis07,
author = {van den Geest, Gerrit},
title = {Constraints for Type Class Extensions},
keywords = {type systems},
school = {Utrecht University},
year = 2007,
month = apr,

}

Atze Dijkstra, Gerrit van den Geest, Bastiaan Heeren, and S. Doaitse Swierstra. Modelling Scoped Instances with Constraint Handling Rules. Note: Rejected by ICFP '07, 2007. Abstract:

Haskell's class system provides a programmer with a mechanism to implicitly pass parameters to a function. A class predicate over some type variable in the type signature of a function induces the obligation for the caller to implicitly pass an appropriate instance of the class to the function. The class system is programmed by providing class instances for concrete types, thus providing, for each class, a unique mapping from types to instances. This mapping is used whenever an instance for a class predicate over some type is required. Choosing which instance to pass is solely based on the instantiated type of the class predicate. Although this mechanism has proved to be powerful enough for modelling overloading and a plethora of other programming language concepts, it is still limited in the sense that multiple instances for a type cannot exist at the same time. Usually one can program around this limitation by introducing dummy types, which act as a key to map to additional instances; but this indirect way of allowing extra instances clutters a program and still is bound to the finite number of types statically available in a program. The latter restriction makes it impossible to dynamically construct instances, which, for example, depend on runtime values. In this paper we lift these restrictions by means of local instances. Local instances allow us to shadow existing instances by new ones and to construct instances inside functions, using function arguments. We provide a translation of class and instance definitions to Constraint Handling Rules, making explicit the notion of ``scope of an instance'' and its role in context reduction for instances. We deal with the ambiguity of choosing between instances by using a framework for heuristically choosing between otherwise overlapping instances.

@unpublished{dijkstra_et_al_scoped_instances_07,
author = {Atze Dijkstra and van den Geest, Gerrit and Bastiaan Heeren and S. Doaitse Swierstra},
title = {Modelling Scoped Instances with Constraint Handling Rules},
abstract = { Haskell's class system provides a programmer with a mechanism to implicitly pass parameters to a function. A class predicate over some type variable in the type signature of a function induces the obligation for the caller to implicitly pass an appropriate instance of the class to the function. The class system is programmed by providing class instances for concrete types, thus providing, for each class, a unique mapping from types to instances. This mapping is used whenever an instance for a class predicate over some type is required. Choosing which instance to pass is solely based on the instantiated type of the class predicate. Although this mechanism has proved to be powerful enough for modelling overloading and a plethora of other programming language concepts, it is still limited in the sense that multiple instances for a type cannot exist at the same time. Usually one can program around this limitation by introducing dummy types, which act as a key to map to additional instances; but this indirect way of allowing extra instances clutters a program and still is bound to the finite number of types statically available in a program. The latter restriction makes it impossible to dynamically construct instances, which, for example, depend on runtime values. In this paper we lift these restrictions by means of local instances. Local instances allow us to shadow existing instances by new ones and to construct instances inside functions, using function arguments. We provide a translation of class and instance definitions to Constraint Handling Rules, making explicit the notion of ``scope of an instance'' and its role in context reduction for instances. We deal with the ambiguity of choosing between instances by using a framework for heuristically choosing between otherwise overlapping instances. },
year = 2007,
note = {Rejected by ICFP '07},

}

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