Abstract
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 language | English |
|---|---|
| Pages (from-to) | 992-1009 |
| Number of pages | 18 |
| Journal | Theory and Practice of Logic Programming |
| Volume | 17 |
| Issue number | 5-6 |
| Early online date | 22 Aug 2017 |
| DOIs | |
| Publication status | Published - Sept 2017 |
Keywords
- Constraint Handling Rules
- pattern unification
- generic quantification