Higher-order Cons-free Interpreters

Cynthia Kop, Jakob Grue Simonsen

Constructor rewriting systems are said to be cons-free if any constructor term occurring in the rhs of a rule must be a subterm of the lhs of the rule. Roughly, such systems cannot…