Verification of Constraint Handling Rules using Linear Logic Phase Semantics
Rémy Haemmerlé, Hariolf Betz · 2008
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.