Logic programming with α-equivalence

[suhr]

Name binding is an essential part of most programming languages. But it's also a pain spot when implementing programming languages.

One approach to make implementing programming languages easier is HOAS, like in λProlog. Another approach is based on fresh name generation, like in αProlog.

While λProlog approach seems to be suitable for typed logic programming languages, it might be possible to port αProlog approach to Ciao.

UPDATE: I should have provided a paper: αProlog: A Logic Programming Language with
Names, Binding and α-Equivalence

[jfmc]

Thanks for the idea and the pointers! One idea would be to implement the operational semantics (Section 5.2) on top of Prolog's unification using attributed variables, but we'd need to have a careful look at it.