Constraint Handling Rules with Binders, Patterns and Generic Quantification

Alejandro Serrano, J. Hage

Research output: Contribution to journalArticlepeer-review


Constraint Handling Rules provide descriptions for constraint solvers. However, they fall short when those constraints specify some binding structure, like higher-rank types in a constraint-based type inference algorithm. In this paper, the term syntax of constraints is replaced by λ-tree syntax, in which binding is explicit; and a new ∇ generic quantifier is introduced, which is used to create new fresh constants.
Original languageEnglish
Pages (from-to)992-1009
Number of pages18
JournalTheory and Practice of Logic Programming
Issue number5-6
Early online date22 Aug 2017
Publication statusPublished - Sept 2017


  • Constraint Handling Rules
  • pattern unification
  • generic quantification


Dive into the research topics of 'Constraint Handling Rules with Binders, Patterns and Generic Quantification'. Together they form a unique fingerprint.

Cite this