Object level unification


I'm quite new to logic programming and I'm in the process of understanding logical frameworks. Do logical frameworks allow us to use the same unification algorithm at both object and meta levels? If so, what benefits are there? I'm looking for a HO language that supports HOAS; is Twelf and lambda prolog (though it is no longer maintained) the best candidates? How about a language called HiLog? Any other info will be much appreciated.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


Unfortuately, "object and meta levels" have enough different interpretations that I'm not certain what you mean, but I'm decently confident Twelf supports what you're describing. Could you say something more specific about what you're looking for?

I only have a passing familarity with HiLog, but I seem to remember the last time I looked at it that it doesn't support higher-order abstract syntax. If I'm incorrect that's something I'd like to know, though!