Home » forums » LtU Forum

Object level unification

Hi

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.

By daYZman at 2007-10-12 11:08 | LtU Forum | previous forum topic | next forum topic | other blogs | 5534 reads

Comment viewing options

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

Questions

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!

By Rob Simmons at Fri, 2007-10-12 17:17 | login or register to post comments