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

Has anybody ever used (this particular) Shannon?

With traditional notations, it is only practical to express part of the potentially precise information in a precise way. Fixing that problem can relieve a burden of distilling precise information from various informal representations and integrating it.

Types for Atomicity: Static Checking and Inference for Java by Cormac Flanagan, Stephen N. Freund, Marina Lifshin, and Shaz Qadeer:

Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic methods are amenable to sequential reasoning, which significantly facilitates subsequent analysis and verification. This article presents a type system for specifying and verifying the atomicity of methods in multithreaded Java programs using a synthesis of Lipton’s theory of reduction and type systems for race detection. The type system supports guarded, write-guarded, and unguarded fields, as well as thread-local data, parameterized classes and methods, and protected locks. We also present an algorithm for verifying atomicity via type inference. We have applied our type checker and type inference tools to a number of commonly used Java library classes and programs. These tools were able to verify the vast majority of methods in these benchmarks as atomic, indicating that atomicity is a widespread methodology for multithreaded programming. In addition, reported atomicity violations revealed some subtle errors in the synchronization disciplines of these programs.

Recently I was coding up libraries in one of my hypothetical toy languages (I hope I'm not the only one :), and I came across a potentially novel (too me) type feature that might actually make sense. So naturally, I wonder if this has been examined before.

Imagine a simple type constructor Vector[T]. I would like to have Vectors be comparable for equality, but *this* feature is only possible if the actual type parameter T is also comparable for equality.

So we might have some silly syntax like this.

mixin Eq[T] is def? ==(T,T):Bool; end

class Vector[T] mix (Eq when T <: Eq) is
...some stuff...
   --
   -- Compare two Vector[T]'s for equality
   --
   def ==(rhs:Self):Bool = 
      self.len = rhs.len and 
      (_ == _).andmap(self, rhs); -- this compares the elements

...some other stuff...
end

Hopefully one gets the idea. Furthermore, what I really want is not to *require* T <: Eq, but to simply notate and elide the methods that depend upon T <: Eq, most notably avoiding writing a gazillion different Vector[T] classes, each featuring some different interesting quality of T that happens to affect an interesting quality of the resulting Vector[T].

Has any other person smarter than I am explored type systems(other than the "uber search and replace" C++ templates) that feature this kind of "capability parametrized" parametrically polymorphic type system with method elision/disqualification before?

Much thanks,

Scott