[quietplatypus]

How is this different from defunctionalizing and converting to smt backend or prolog engine without higher-order capabilities?

[samth]

Other people have taken that approach, for example the HALO project in Haskell. But the imprecision of the defunctionalizaton often makes it hard to prove the properties you want, especially without static types.

[jsli]

I am looking for papers about converting to prolog backend. Could you name one for me? Thanks.