Lambda the Ultimate

In my work, I've started to think a lot about the role of edge computing (think Opera Mini) in applications (and potentially the role of CDNs). My guess is that it's a very constrained C/C++ world right now, outside of some projects like maybe Flux (though it is currently targeted at traditional data centers).

More of a shot into the dark than usual for me, but any suggestions of where to look for orchestrating and benefiting from these? A lot of it is closed/proprietary right now, making it a bit hard to google. One direction to look into is IDS implementations and smart routers, but these seem to be along a slightly different evolutionary path...

Noam (uid 3913) announced on his weblog at the beginning of the year a technique that allows one to bridge the gap between meta-theoretic notions of function space and theory-internal notions, in a way that is compatible with structural induction over Higher-Order Abstract Syntax, by applying Reynolds' Definitional Interpreters for Higher-Order Programming Languages [pdf] (cf. LtU classic), and realised it as an implementation in Twelf.

That's a lot of ideas in one sentence, but since HOAS is in the air this month, I guess there are a good number of LtUers who will want to get to grips with this stuff.

Refs:

• Defunctionalizing Proofs: Noam's original announcement;
• The follow-up weblog post, with scholarly write-up;
• The code.

Hi everyone!
Thanks for reading my topic!
If you know about Indexing Model, Please let me know the difference between PAT tree and Inverted index in Search Engine indexing model
(Store Capacity, Speed Access, Edit ...)
And finally which one should choose?
Thanks
Best regards