Coinductives Semantics for Constraint Handling Rules

May 4, 2010

Rémy Haemmerlé


Coinductives Semantics for Constraint Handling Rules

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Constraint Handling Rules (CHR) is a concurrent committed-choice rule-based programming language introduced in the 1990s by Fruehwirth. While it has been originally designed for the design and implementation of constraint solvers, it has come into use as a general-purpose concurrent programming language. CHR shares with its spiritual ancestor, Constraint Logic Programming (CLP), nice declarative semantics consisting in a direct translation into logic. However, whereas fixpoint semantics is an important foundation of CLP, there is no equivalent notion for CHR that captures behaviors of the whole language. In this talk we will shortly present CHR and its logical semantics. Then we introduce a simple fixpoint semantics based on a biggest fixpoint computation. Finally we show the resulting language is an elegant framework to program using coinductive reasoning on infinite objects.